@slowcoding@social.vivaldi.net @davidlowryduda@mathstodon.xyz Note that these successes are not the LLM alone. The LLM constructs a series of Lean proof objects, that can be verified by Lean. In other words, there is an absolute source of truth, and the system can reliably build on its lemmata (or keep fixing the sub-proofs, until they pass muster). This interaction is quite productive. ATPs in somewhat similar frameworks are also quite good, but we never threw that amount of compute at them.