To be fair, however, these proofs are using several of the automatic proving methods built into Lean, like linarith, nlinarith, field_simp, and so on. Each of these are hundreds of lines of manually tweaked heuristics.
It's still quite interesting. I think if we had a good integration of AI methods into the Lean runtime itself the theorem prover could be excellent. You could have a cooperative model where the human mathematician writes down statements, and the AI fleshes out a proof or catches typos that you make. Right now Lean has similar functionality but the automatic proving isn't as good as it could be.
I just wish the Lean community wasn't stuck on the Lean 3 -> Lean 4 migration for the past year. I'm getting flashbacks of Python 2 -> Python 3 ....
This is definitely something that we'll be looking into more closely in the future. Our old and busted `gptf` tactic was a good start but we can do much better!
I may be misunderstanding, but it seems like gptf can only apply theorems from the set you guys trained it on ... in which case I don't see how it could possibly help with the development of a theory beyond its first few statements. Have I got that right? and if so is it something that might be addressed in future iterations?
How long (or how much compute resources) does it take to solve one of these IMO problems right now? My estimation is that just the time to run tactics linarith for many different cases would be significant enough to make it too slow to do interactively, but I'm curious to check my guess.
It takes a lot of CPU (lean side) on top of GPU (neural side) indeed. But technically, when properly parallelized, it takes no more than 1-2h to crack the hardest problem we've cracked so far.
To be fair, however, these proofs are using several of the automatic proving methods built into Lean, like linarith, nlinarith, field_simp, and so on. Each of these are hundreds of lines of manually tweaked heuristics.
It's still quite interesting. I think if we had a good integration of AI methods into the Lean runtime itself the theorem prover could be excellent. You could have a cooperative model where the human mathematician writes down statements, and the AI fleshes out a proof or catches typos that you make. Right now Lean has similar functionality but the automatic proving isn't as good as it could be.
I just wish the Lean community wasn't stuck on the Lean 3 -> Lean 4 migration for the past year. I'm getting flashbacks of Python 2 -> Python 3 ....