G\"odel's Poetry

TL;DR

This paper presents a novel multi-agent system employing specialized language models and recursive decomposition for automated theorem proving in Lean4, significantly improving success rates over previous methods.

Contribution

It introduces a multi-agent architecture that combines autoformalization, proof generation, and recursive theorem decomposition, extending the Kimina Lean Server with AST parsing capabilities.

Findings

Achieves 90.4% pass rate on miniF2F without decomposition

Significant improvement with theorem decomposition

Open-source implementation available on GitHub and PyPI

Abstract

Formal, automated theorem proving has long been viewed as a challenge to artificial intelligence. We introduce here a new approach to computer theorem proving, one that employs specialized language models for Lean4 proof generation combined with recursive decomposition of difficult theorems into simpler entailing propositions. These models are coordinated through a multi-agent architecture that orchestrates autoformalization (if required), proof generation, decomposition of difficult theorems into simpler entailing propositions, and recursive proof (and/or decomposition) of these propositions. Without decomposition, we achieve a 90.4% pass rate on miniF2F. With decomposition, this is significantly improved. A key technical contribution lies in our extension of the Kimina Lean Server with abstract syntax tree (AST) parsing capabilities to facilitate automated, recursive proof decomposition. The system is made available on PyPI as goedels-poetry (at https://pypi.org/project/goedels-poetry ), and the open-source implementation KellyJDavis/goedels-poetry (at https://github.com/KellyJDavis/goedels-poetry ) facilitates both adaptation to alternative language models and extension with custom functionality.