@slowcoding@social.vivaldi.net
2026-09-09 21:11 UTC
@StephanSchulz@fosstodon.org @davidlowryduda@mathstodon.xyz ok, but is that an inherent problem with how these tools work? Have we ever tried to throw as much compute to them as we are doing with LLM (training+inference)? How would they scale?
LLMs sound like clever random walks in the solution space whereas these tools sound like systematic explorations. Is there more to it fundamentally ?
Replies (1)
-
@StephanSchulz@fosstodon.org 2026-09-10 13:46
@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.