2 ms·
Maybe before we have AGI we should get an AI that can translate Andrew’s proof into Lean for us. Easily tractable, checkable, useful, and build-upon-able
by ljlolel 1y ago
Maybe before we have AGI we should get an AI that can translate Andrew’s proof into Lean for us. Easily tractable, checkable, useful, and build-upon-able
- grumbelbart2 1y agoWork is already underway in that direction: https://github.com/deepseek-ai/DeepSeek-Prover-V2 https://github.com/deepseek-ai/DeepSeek-Prover-V2 but also https://deepmind.google/discover/blog/alphaevolve-a-gemini-powered-coding-agent-for-designing-advanced-algorithms/ https://deepmind.google/discover/blog/alphaevolve-a-gemini-p... Terence Tao is doing a lot of work in this direction.
- zozbot234 1y agoKevin Buzzard is reportedly working on formalizing a modern proof of FLT. This effort has already managed to surface some unsound arguments in one of the prereqs for the proof (namely crystalline cohomology) https://xenaproject.wordpress.com/2024/12/11/fermats-last-theorem-how-its-going/ https://xenaproject.wordpress.com/2024/12/11/fermats-last-th... though the issue has since been fixed.