FLT: Anthropic has beaten me to it
26 points by lalitm
26 points by lalitm
An existing mechanization, even if barely-comprehensible slopped-out code, destroys the possibility for funding future work
Has anyone before funded specifically idiomatic proof, or just a proof verification and the mathematicians cared about the format? (Feels similar to companies paying developers for results and developers potentially caring about the readable code)
Has anyone done attempts at forcing an idiomatic translation? Basically, is the issue with the current model capabilities, or with approach taken?
Yes, per the OP:
I am currently being funded by the EPSRC to formalize a proof of Fermat’s Last Theorem, and a naive reaction to the news above is that I no longer have any work to do. This is not the case. The work certainly achieves some of the aims of the EPSRC project [...]. But I also promised several other things to EPSRC: firstly, that I would be making pull requests to Lean’s mathematics library, adding fundamental objects from modern number theory; this is ongoing.
The "Mathematical details" paragraph is a fascinating account of what constitutes an elegant proof.
As the author notes, there is value in "building the commons", by contributing formalisms to Lean's mathlib. I hope their work continues: https://github.com/ImperialCollegeLondon/FLT