Lean proof refactoring entry scores 86.31 points under US$3 per problem

Researchers report in a preprint that their automated Lean proof refactoring entry scored 86.31 points across 60 final problems, compared with 33.33 for reference proofs. It cost US$166.33 at list prices, counting every call, and placed 8th at the deadline. The system selected models for individual stages using measured performance per dollar and applied programmatic rewrite rules checked by the compiler. Spending averaged US$2.772 per problem and reached at most US$2.874, below the US$3 cap. Rules fixed before release added 0.93 points; gains from later passes were measured in sample.