Comment by mikmoila
13 hours ago
"The effort succeeded when we switched to using Prove2Me, an open collaborative platform for formalizing mathematics designed by Tianyi Peng and his collaborators at Columbia University."
So in the end, it required tooling crafted by humans.
I was involved in building https://prove2.me (but I am not affiliated with Anthropic nor involved in anything related to FLT). I think the key insight in prove2me is to prove theorems "top-down", which allows a large number of users to collaboratively work on a single theorem statement. This setup also seems to work well for a "swarm" of agents. I posted more of my thoughts on the Lean Zulip.
There's nothing about prove2me that couldn't have been coded just like any other huge coding project frontier models have proven themselves extremely good at doing. It just happened to have been made by humans.
By this standard, no computer has ever accomplished anything, because humans built the computer. AI bubble about to burst any second now.
Humans built the tool which enabled the result. AI used the tooling for eliminating the dead ends. Yes, I can appreciate the practical value of all this, but IMHO it is not a kind of breakthrough result the article gives impression of.
A literal rock we carved patterns on and shot lightning into has accomplished something no human has.
How much more magical do you want this to be?
Tool or not it did something you could never have accomplished.
7 replies →
For now. That, too, will change in the future.
Same thing was said about cryptocurrency for like 15 years: "_in the future_ it will replace all fiat currency".
AI ≠ crypto.