Case study: proving sqrt(2) irrational with LPTP and an LLM
Fred Mesnard, Étienne Payet, Wim Vanhoof
AI use, as the source states it
“We end up with a complete formal proof, partially generated by an LLM and fully proof-checked by LPTP.”
Named here, or see a mistake? Write to privacy@papex.org.