Neural Theorem Proving (NTP) employs Large Language Models (LLMs) to automate formal proofs in proof assistants.
While LLMs have achieved relatively remarkable success in informal reasoning tasks using natural languages, the transition to mechanized formal theorem proving presents persistent challenges.
Mechanized proof languages often contain many syntactic constructs and diverse, specialized proof tactics, which facilitate expert use but have no direct counterpart in informal mathematical proofs.
These prover-specific idioms represent an additional burden for LLM-based NTPs that might be otherwise successful in generating informal proofs.
Seeking to bridge this gap between formal proof construction and informal reasoning, in order to better facilitate NTP, this work approaches these challenges from a language design perspective.
We look at common reasoning patterns in informal proofs and in existing mechanized proofs, and design Minilang (formally named Isabelle/Minilang), a minimalist proof language that captures these reasoning patterns.
In contrast to proof languages (informal and formal) that often feature a large collection of operations with unclear semantic boundaries, Minilang is deliberately kept minimalist — its core design comprises only 10 proof operations, each with clear semantic distinctions.
We further develop a rule-based translator from Isabelle's proof language (Isar) to Minilang, translating ~340,000 existing Isabelle proofs with an ~85% success rate.
Using this translated corpus, we finetune two LLMs to compare machine learning performance on Minilang versus the original Isar language.
Experiments show Minilang benefits the two LLMs by improving the pass@1 success rate on the PISA benchmark by up to 20/29 percentage points in comparison to the Isar-based LLMs w/wo Sledgehammer.
The pass@1 rate reaches 69.1%, exceeding the prior work Baldur's pass@64 (65.7%); the pass@8 rate reaches 79.2%, exceeding the state-of-the-art on PISA (71.0%) achieved by Magnushammer.