On Some Problems from the Kourovka Notebook
Wouter van Doorn, Elias Judin, Pietro Monticone, Daniel Morrison
AI use, as the source states it
“All of these solutions were autonomously discovered and formally verified in Lean by Aristotle, a formal reasoning agent developed by Harmonic.”
Model: Aristotle, as stated
Named here, or see a mistake? Write to privacy@papex.org.