|
|
|
|
|
|
by maxwells-daemon
1659 days ago
|
|
|
Automated theorem proving + neural language models + reinforcement learning. I think most people seriously underestimate how powerful modern proof assistants like Lean [1] are for building things like provably correct software and chips, as well as verifying math research. But fully formalizing anything big leads to a proliferation of small annoying lemmas -- not "difficult" to prove per se, just annoying and time-wasting. I'm working on a neural theorem prover that aims to solve these lemmas fully automatically. [1] https://leanprover.github.io/ |
|
|