Proving at Scale for Universal Algebra
João Araújo, Jan Hůla, Mikoláš Janota, Edmond W. H. Lee, Bartosz Naskręcki
AI use, as the source states it
“LLM-guided agents search for these proofs; a referee agent rebuilds them from source, and the Lean kernel checks the resulting corpus in a final audit.”
Named here, or see a mistake? Write to privacy@papex.org.