MechGeo: Autoformalizzazione e dimostrazione della geometria euclidea in Lean 4

I ricercatori hanno introdotto MechGeo, un framework che automatizza la formalizzazione e la dimostrazione di problemi di geometria euclidea utilizzando l'assistente di dimostrazione Lean 4. Il framework è composto da due componenti principali: GeoFormalizer, che traduce problemi geometrici informali in una rappresentazione strutturata chiamata GeoIR e poi in codice Lean 4, e GeoProver, che costruisce piani di dimostrazione e deriva lemmi intermedi. GeoProver può algebraizzare selettivamente i sotto-obiettivi, utilizzando strumenti esterni come Singular o SymPy per generare certificati algebrici, ma tutte le dimostrazioni sono infine verificate dal kernel di Lean. Negli esperimenti con sette backbone LLM, MechGeo ha migliorato significativamente l'autoformalizzazione, specialmente per i modelli con capacità di traduzione diretta più deboli. Su un insieme di 43 problemi storici di geometria IMO, GeoFormalizer ha generato dichiarazioni formali che GeoProver ha dimostrato in 29 casi. Il framework è progettato per essere nativo di Mathlib, il che significa che si integra con la libreria matematica esistente di Lean. Questo lavoro affronta la sfida di convertire fedelmente dichiarazioni matematiche informali in dimostrazioni verificabili da macchina, un passo chiave per l'uso dell'IA nella matematica formale.