News · 2026-09-19

GPT-6 Astra helps solve FrontierMath's first Major Advance problem

Epoch has recorded its first solved FrontierMath Open Problems Major Advance entry: a proof that every approval-based committee election has a core-stable committee. The achievement matters because Epoch credits GPT-6 Astra with the central idea and proof in an interactive collaboration, while explicitly refusing the more dramatic claim that the model solved the problem autonomously.

Key facts

• The Epoch problem page lists the result as the only solved problem among six Major Advance entries.
• The paper is arXiv:2609.11912, submitted September 10 by Patrick Becker, Matthias Greger and Dominik Peters.
• The original challenge asked for an election with an empty core; the proof shows no such counterexample exists.
• Epoch labels the provenance human plus AI, not autonomous AI.

Approval-based committee elections ask voters to approve candidates and choose a representative committee. The core is a stability idea: no sufficiently large coalition should be able to credibly complain that another committee would serve it better. The open problem requested an example where every possible committee could be blocked. Becker, Greger and Peters instead proved a stable committee always exists.

The paper introduces a harmonic-entropy objective over committees and voter payment systems. In rough terms, it searches for an allocation that does not leave a coalition with a compelling improvement. The authors show that if a candidate swap could improve the objective, the committee was not at the appropriate local optimum; a local optimum satisfies a stronger core-plus condition and therefore ordinary core stability. They also give a polynomial-time local-search method.

The headline number is one: this is Epoch's first Major Advance solution, not a routine benchmark item. But the provenance qualification matters more. Epoch says Astra supplied the primary idea and proof during a long session with the named researchers, and also says it could not solve the task from a simple prompt. That is a picture of AI as a high-leverage mathematical collaborator: generating a route through an argument while humans select, interrogate and formalize it.

The paper says its existence result was formally verified in Lean using the authors' ABCVotingLean repository. A proof assistant is like a compiler for logical steps: it will reject an unstated leap that a human reader might wave through. Formalization materially improves confidence in the encoded theorem, but it does not substitute for independent peer review, validation of every modeling choice or a claim that the model discovered the theorem alone.

The strongest counterargument is that a solved problem whose requested counterexample is impossible is an unusual benchmark outcome, and a human-guided proof should not be counted as autonomous scientific discovery. Epoch agrees enough to create its human-plus-AI category. That restraint is the story's value. It points toward a better metric than a binary solved/not-solved leaderboard: how much proof assistants and humans were needed to turn an AI insight into durable knowledge.

Primary source, verified: read the paper → (arXiv 2609.11912)

Ground Truth. (2026, September 19). GPT-6 Astra helps solve FrontierMath's first Major Advance problem. Ground Truth. https://groundtruth.day/news/frontiermath-core-approval-committee-elections.html

@misc{groundtruth:frontiermath-core-approval-committee-elections,
  title  = {GPT-6 Astra helps solve FrontierMath's first Major Advance problem},
  author = {{Ground Truth}},
  year   = {2026},
  month  = {sep},
  url    = {https://groundtruth.day/news/frontiermath-core-approval-committee-elections.html}
}

Topics: research · mathematics · reasoning · frontiermath · proof-assistants