Doktorandské kolokvium KAI - Ján Pastorek (19.10.2026)
v pondelok 19.10.2026 o 13:10 hod. v miestnosti I 9
Prednášajúci: Ján Pastorek
Názov: AI4math. Towards automated graph theory? A quest for interesting mathematical questions and conjectures in the age of AI.
Termín: 19.10.2026, 13:10 hod., I 9
Abstrakt:
OpenAI, Google DeepMind and Anthropic, along with their LLMs have undeniably demonstrated that math problem solving can be done at scale. Yet, the true open frontier remains autonomous discovery, i.e., knowing which questions are worth asking in the first place. Left unconstrained, computational discovery systems do not fail by getting stuck. They fail by drowning researchers in an "avalanche of triviality," producing potentially millions of technically true but mathematically uninteresting statements.
In this talk, we present results from our recent paper, where I introduce AutoGraphForge, a pipeline designed to autonomously hypothesize, refute, formalize, and verify conjectures in graph theory. The goal of this pipeline has been to find interesting conjectures that cannot be easily proved or disproved by such autonomous computational effort. To separate genuine mathematical interesting statements from combinatorial noise, the system couples counterexample-guided generation with a linear-programming novelty filter to eliminate consequences of a database of known theorems (knowledge base). It then subjects candidates to active counterexample search across hundreds of thousands of (extremal) graphs from our best graph-theoretical databases and by algorithms such as simulated annealing that modify graphs to find such counterexamples. The remaining statements are then exported to the Lean 4 proof assistant to be verified with the help of Lean hammers and LLMs. All partial results such as the effort spent and counterexamples are collected to help us look back and get insight. The hope is to get potentially interesting and somewhat computationally nontrivial statements worth further attention and research.
Finally, we will discuss what truly makes a mathematical question interesting.