“I hesitate to use the word ‘revolutionary,’ but lowering the cost of anything by four orders of magnitude is revolutionary.”
The four orders of magnitude rest on a guess that research math takes 20 times the effort of textbook math. That guess produces 132,800 person-hours to compare against OpenAI’s 17. The Lean proof checks the steps. It does not check that the formal statement matches what OpenAI says it proved.