Simon Frieder hanko Simon Frieder

A short history of the Lean Comparator

2026-10-03

At the bottom of the Lean Comparator’s GitHub page, a small acknowledgement contains this text: “Comparator was originally developed by Lean FRO, with feedback from the AIMO team, in support of the AIMO series of competitions and their goal of enabling trustworthy LLM Lean evaluation on Kaggle.”

FYI, for fixed theorem statements, the Comparator compares an untrusted solution against a trusted challenge, checks the permitted axioms, and rechecks the proof through the kernel. These guarantees depend on its documented trust and sandboxing assumptions. It gives an evaluator a way to check that a submission proves the specified formal statement under the allowed assumptions (such as which axioms are used).

There is a little history behind that acknowledgement that I’d like to outline in this post.

We were considering a formal version of the AIMO competition in early 2025, in which models would submit proofs in Lean. That raised a question we needed to settle before trusting a leaderboard: how could we ensure that an LLM-generated submission had actually proved the intended theorem?

I emailed Lean FRO to ask whether there was a gold-standard solution. My concern, loosely put, was that a model might find a way to “trick the kernel”. Even then, it seemed clear that we had to anticipate reward hacking if we ran such a competition. At that time, AIMO2 was running, and we already had over a thousand teams and thousands of submissions. It didn’t seem unreasonable that a formal variant might attract even more attention. Perhaps a determined LLM might come up with tricks significantly more sophisticated than just sorrying a theorem (there are such tricks!). Note that early 2025 was a very different LLM era: it wasn’t yet clear whether LLMs would be able to consistently solve IMO problems. We first showed this in March 2025, though this largely flew under the radar. Today, the IMO25 announcements are what most people believe to be the “hour zero”, though this is, strictly speaking, wrong. And whether LLMs might be able to — and reward hacking in such a challenging environment isn’t straightforward, though these days it is clear it can happen.

Lean FRO did a great job building the tool for us, and I believe we were their first “customers”, as a person from the Lean FRO team was explicitly assigned to help us devise this after I had approached them. Our role was to explain the competition requirements, provide feedback, and then work towards getting it running on Kaggle, which we did.

The formal competition itself sadly did not ultimately materialize. There were several reasons, all longer than the margins of this blog to spell out, including the difficulty of finding enough formalizers with sustained availability. The market at the time for formalizers was extremely tough and very much a sellers’ market: by now, it seems that things have relaxed dramatically because the data the formalizers generated at the time seem to have brought about the current revolution in autoformalization by frontier models, which to a degree have solved this problem (though open-weight—and even more so, open-source—LLMs have yet to catch up). We did, however, receive excellent support from people such as Joseph Myers, who helped us formalize a few problems. To run a competition at the level of quality that we wanted, for better or worse, it’s necessary to also formalize the proofs of the theorems, not just the statements, even though only the statements would be needed to run the competition.

But the work on evaluation did produce a concrete result: we got the Comparator running on Kaggle and carried out a successful trial. So anyone considering a future Lean-based competition on Kaggle now has something to build on, as there is now in-house knowledge at Kaggle on this. We worked with them to get the integration off the ground, even though we did not end up running the competition, and if you ever run such a competition, feel free to ask me about this :) Probably only a version refresh would be needed.

These days, it is particularly pleasing to see the Comparator being used beyond that original competition setting and to know I played a role in getting its development started before it spread through the community. A few examples in which I was happy to see Comparator in action: