So many questions about the sole type theory result dropped by OpenAI last night. Need time to think. In the meantime, I found the Lean code, but where is the comparator challenge? I want to vet definitions and theorem statements. Also, the proof appears to use classical reasoning many times. Has this been a barrier for type theorists? Do we want to look for a constructive proof here, or does it not really matter? github.com/openai/math/tree/ma…
Similar posts
2 posts close in meaning, closest first
Oh and also, just when everybody thought auto-formalisation is a solved problem, only about half of the 722 papers even have a formalisation… ?
#openAI released more than 700 Theoremoids: github.com/openai/math/tree/ma… It does include Hilbert’s 10th problem over QQ right on the first page which I have also been prompting (only half-jokingly): machteburch.social/@tomkalei/1… mathe.social/@tomkalei/1172302… So it’s undecidable… told you so.
