130k Lines of Formal Topology: Simple and Cheap Autoformalization for Everyone?
31 points by PaulHoule
by bmenrigh
2 subcomments
My main skepticism here is whether the theorems have been properly replicated in the proof. Verifying that the proof really captured the mathematical statement seems like a manual, human process, and quite hard to repeat reliably across proofs.
by timmg
0 subcomment
This is so cool. I think I had read that some mathematicians were trying to formalize all(?) known math in Lean. Expecting it to be a long term project. And I was recently wondering how long it would be before they turned LLMs loose on the problem.
Seems like plenty of people are already on the path. So cool.
by QuesnayJr
0 subcomment
What's most impressive about it is that it uses a system, Megaladon, which is pretty obscure. There isn't that much documentation or examples, but it can still formalize an advanced undergraduate textbook.
by esafak
1 subcomments
Are there any lessons or tricks here that we can apply to software engineering? What kinds of assertions can we express more easily with Lean etc. than with unit tests, fuzz tests, property tests, using our existing testing frameworks?
Hacker News