Compile to Compress: Boosting Formal Theorem Provers by Compiler Outputs

Guchan Li, Rui Tian, Hongning Wang

Large language models (LLMs) have demonstrated significant potential in formal theorem proving, yet state-of-the-art performance often necessitates prohibitive test-time compute vi…