Show HN: Acorn, a theorem prover with built-in AI

For a while I've been interested in mathematical theorem proving. It just seems like the sort of thing that a computer should be able to do. Or at least to help check your math.

But it's just hard to use theorem provers. Even for someone who has used regular programming languages. You typically have to remember many different theorems and tactics, even to prove "basic things" that people would usually just assert without explanation.

Acorn is an attempt to fix this problem, to make a theorem prover that's as easy to use as a regular programming language. A "Python for theorem proving".

Acorn includes an AI model, but a small one, that runs on your machine. The whole thing runs as a VS Code extension, so it's easy to install.

If you've ever used a theorem prover before and found it interesting but annoyingly difficult, Acorn is for you. Check it out and I'd love to hear your feedback.

Thanks!