2026-09-10 13:46 UTC
@slowcoding@social.vivaldi.net @davidlowryduda@mathstodon.xyz I don't think there is a fundamental problem, but we probably need a proof planner on top of the ATPs (note that for many Proof Assistants, ATPs, as "Hammers", routinely do much of the heavy lifting). The field has never been remotely as well funded as "AI" is now, and while we do use as much CPU as we can get, no-one has 10000 machines available for experimentation and tuning.
Replies (1)
-
@slowcoding@social.vivaldi.net 2026-09-10 16:11
@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?