現代の定理証明システムは高い性能を発揮するために膨大な計算資源を必要としています。これは検証済みの証明データが希少であり、形式証明探索の長い推論トレースが必要とされることが主な原因です。結果として、教師あり微調整（SFT）とサンプリングの両方が計算量的に非常に高コストになっています。こうした課題に対応するため、研究チームはPythagoras-Proverという計算効率に優れたオープンソースのLean定理証明器ファミリーを開発しました。実用的な計算予算内で動作することを目標として設計されています。 このプローバーファミリーは2つの生成パラダイムを採用しています。4Bと32Bパラメータの自己回帰モデル、および反復的にLean証明を改善する4B拡散ベースプローバーの概念実証版です。訓練効率を高めるため、研究チームは簡単、中程度、難問題に階層化されたLean検証コーパスを構築し、カリキュラム学習によって短くシンプルな証明から段階的にスキルを習得させます。訓練中には動的証明推論フィルタリングスキームを採用し、情報量の多い証明トレースを保持しながら、各インスタンスを8kトークンの文脈予算内に収めています。 さらに、Augmented Lean Formalisation（ALF）という革新的な手法を導入しました。希少な検証済みコーパスを自己蒸留により形式的に検証されていない変異体へと拡張し、追加の訓練信号を得ることができます。既知の問題を摂動させながら形式的な特性を保つことで、表面的な形式への依存を軽減します。 実験結果は顕著です。Pythagoras-Prover-4Bは約167倍少ないパラメータながらMiniF2F-Testでpass@32において86.1%の精度を達成し、671Bパラメータを持つDeepSeek-Prover-V2の82.4%を上回りました。一方、Pythagoras-Prover-32BはMiniF2F-Testでオープンソースの最先端となる93.0%の精度を記録し、PutnamBench問題672問中93問を解くことに成功しています。研究チームはALF変異ベンチマークMiniF2F-ALFもリリースしており、ここでも同モデルの優位性が確認されています。