Mathematics Distillation stage 2

The challenge concluded on the last day of August, and the main leaderboard has now been released. Basically, the task was to come up with a script that automatically proves an equational implication or generates a counterexample to it(thus disproving it). The hard part was producing a valid lean certificate for each proof or counterexample.

One interesting part about the challenge is the explicit incorporation of LLMs, which could be called when no deterministic strategy worked within the time/resource limits. The caveat is that they are pretty weak LLMs by current standards, and not your almighty Fable/Astra. The hope, then, was that slipping a tiny “cheatsheet” into the prompt would help them orient themselves better and come up with correct proofs.

Well, in the end it didn’t, at least not with any of the strategies I tried. Here’s a complete flowchart of my final solver:

As you can see, the LLM is only called at the very end of the chain, when everything else has failed. Furthermore, in offline tests, the LLM never closed a single implication that the deterministic strategies couldn’t. Why are LLMs unable to help here despite the evidence of their improved abilities reported in arXiv:2509.20820?

I think here a naive approach fails because LLMs already understand perfectly well what the task is: what a magma is, how an implication is proven. Writing the Lean statements correctly is probably the only part where a cheatsheet of correctly written Lean could help. At a higher level, though, the most difficult implications are usually the ones requiring either searching through very large counterexamples or using strategies that apply to only a handful of implications. Those are precisely the kind of things you don’t fit in a cheatsheet: the former is too large, while the latter is not uniform. A cheatsheet works best when a small set of rules is enough to finish the task. Here it’s exactly the opposite: the problem description is uniform(easy to explain in a few sentences to humans and LLMs alike), but the magmas themselves are not.

This doesn’t show, however, that we can’t distill mathematical reasoning into a compact and human-readable artifact. Maybe for other types of mathematical reasoning we can. Maybe for other classes of weak LLMs we can. Or maybe we can for thinking models not based on LLM architecture and its probabilistic, generative way of producing responses. There’s more to explore here.