L'API Aristotle supporta la formalizzazione in Lean 4 del problema della cavalletta dell'IMO 2009

Un recente preprint su arXiv (2605.20120) presenta un caso di studio che utilizza l'API Aristotle per assistere nella dimostrazione di teoremi in Lean 4, affrontando specificamente il problema della cavalletta (IMO 2009, Problema 6). L'artefatto generato dall'IA enuncia una versione generalizzata del teorema in Lean e presenta quattro lemmi verificati che affrontano aspetti locali di una strategia di scambio basata su massimalità e scambio adiacente. Questi lemmi dimostrano che la somma parziale finale corrisponde alla somma totale, che una trasposizione adiacente influenza solo la somma parziale intermedia rilevante, che la somma parziale modificata assume la forma prevista e che la massimalità in una posizione che consente uno scambio con un successore adiacente impone una corrispondente condizione proibita. Tuttavia, il teorema principale rimane non dimostrato, contrassegnato da un 'sorry' irrisolto. Questo studio sottolinea sia i punti di forza che le debolezze della dimostrazione assistita dall'IA nella matematica a livello olimpico.