@slowcoding@social.vivaldi.net
2026-09-10 16:11 UTC
@StephanSchulz@fosstodon.org @davidlowryduda@mathstodon.xyz ok thanks. So at that point, OpenAI and Anthropic exhibiting these new advancements in Maths could be a display of their resources more than a proof of their potential in terms of reasoning…
In other words, we have no benchmark to understand how big a breakthrough (if it’s one at all) this is, right?
Replies (1)
-
@StephanSchulz@fosstodon.org 2026-09-10 18:32
@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.