{"id":"b4064b21-2254-4584-afe9-6ba9e94a2c51","arxiv_id":"2412.10673","paper_version":1,"verdict":"CONDITIONAL","confidence":"MODERATE","novelty_score":7.0,"correctness_risk":"medium","formal_verification":"none","parameter_count":2,"one_line_summary":"TongGeometry solves every problem in the IMO-AG-30 geometry benchmark and uses its search engine to propose olympiad problems, several accepted by real competitions.","lead":"An AI system called TongGeometry reports solving all 30 past International Mathematical Olympiad geometry problems in the standard IMO-AG-30 benchmark, surpassing the average gold medalist score, and generating billions of new geometry theorems. It also proposed problems that were shortlisted or selected in real 2024 olympiad competitions, suggesting machines can both create and solve olympiad-level geometry.","discovery_kind":"new_method","skeptic_critique":{"model":"deepseek-v4-flash","headline":"30/30 rests on an unverified custom proof calculus: the rule set is not specified, no verifier or code is released, and only one of thirty traces has been human-checked.","rationale":"The reader's weakest assumption identifies exactly the deductive-database soundness gap, and the reader's CONDITIONAL verdict is appropriate. My pass adds a sharper form: the proof traces are the only direct evidence for the headline, yet the inference rules behind them are not defined, not formalized, and not checked by any external verifier. The Limitation paragraph in the Supplementary also admits that the models 'fall short in sequentially constructing a series of interrelated actions,' which is precisely the ability needed for the hardest IMO solves; independent verification would resolve the tension. I considered and set aside as secondary: the MO-TG-225 text says 225 problems selected from a pool of 196 examples, a numeric inconsistency that weakens the secondary benchmark claim but not the IMO-AG-30 headline; and the translation from natural-language IMO statements to the custom DSL, which is a real risk but is subsumed by the general absence of verifiable artifacts. A non-finding would be unjustified here because the evidence is only as strong as the unverified rule system. If the proposed check passes, the claim becomes strong; if it fails or cannot be run, the correct verdict is at most CONDITIONAL and arguably REJECT until artifacts are released.","tokens_in":14793,"tokens_out":5845,"duration_ms":56484,"concrete_test":"Ask the authors to release both the rule definitions and the 30 solved proof traces, and have an independent group re-run TongGeometry's solver on IMO-AG-30 with a verifier that checks each trace step against the original statement using an independent algebraic engine (Wu's method or Gröbner/CAD). If all 30 traces verify, the 30/30 claim is supported; any failure invalidates it.","verdict_should_be":"UNCHANGED","load_bearing_attack":"The central claim---solving all 30 problems in IMO-AG-30 and outperforming the gold-medal average---requires that every 'solved' trace be a valid proof of the original problem. The supplementary 'IMO 2024 P4 Full Solutions' shows traces in a custom DSL whose inference rules (eqangle, eqcircle, contri, simtri, eqline, midp) are never given a formal semantics in the paper. In particular, rules such as 'eqcircle (...) because eqangle (PCY, PZY)' derive concyclicity from angle equality; without a stated treatment of orientation and degeneracies, such a rule can be false on special configurations. The paper reports no soundness proof for the deductive database and no machine-checked certificates; code and data are not released. Only the IMO 2024 P4 proof was reviewed by a human gold medalist; the other 29 traces have no independent check. The author-stated limitation in the Supplementary ('current models still fall short in sequentially constructing a series of interrelated actions') makes it especially important to verify the hard multi-step solves. I am not asserting the rules are unsound; I am asserting that the current evidence does not establish their soundness, and one invalid rule anywhere would break the 30/30 claim and the 6.7-billion-theorem count derived from the same engine.","agreement_with_reader":"agree"},"referee_report":{"model":"deepseek-v4-flash","summary":"The paper introduces TongGeometry, a Euclidean geometry system that combines a deductive-database engine with fine-tuned LLM policy and value models inside a tree search. The authors claim three main results: (1) the discovery of 6.7 billion geometry theorems requiring auxiliary constructions, including 4.1 billion with symmetry; (2) the proposal of 10 olympiad-style problems, of which one was selected for the 2024 National High School Mathematics League (Beijing) and two were shortlisted for the 2024 US Ersatz Math Olympiad; and (3) state-of-the-art solving performance, including solving all 30 problems in the IMO-AG-30 benchmark within 38 minutes on a consumer-grade machine, thereby surpassing the average IMO gold-medal score, and solving 183 of 225 problems on the self-curated MO-TG-225 benchmark.","tokens_in":15033,"tokens_out":4579,"duration_ms":43417,"significance":"If the 30/30 claim is correct, this is a notable milestone: it would be the first reported system to outperform the average IMO gold medalist on IMO-AG-30, and it would demonstrate an integrated pipeline for both proposing and solving olympiad geometry. The paper's strengths include a strong efficiency story (32 CPU cores and one GPU), a transparent solve-time table for all 30 problems, real-world acceptance of proposed problems, and an expert human check of at least one proof. However, the central evidence is currently not independently verifiable: no code, data, or formal proof certificates are released, the domain-specific language is not given a formal semantics, and only one of the 30 proof traces is reproduced in the supplement. The significance of the paper therefore hinges on verification artifacts that are not yet provided.","major_comments":[{"comment":"The headline claim that TongGeometry 'successfully proved all 30 problems' in IMO-AG-30 is not independently checkable. The paper provides only one full proof trace (IMO 2024 P4) and states that a 2024 IMO gold medalist deemed that proof correct. The inference rules in that trace, such as deriving eqcircle from eqangle in steps [25], [27], [36], and [37], are not given a formal semantics; in particular, the treatment of oriented versus undirected angles and of degenerate configurations is unspecified. Because an unsound rule anywhere in the deductive database would invalidate not only the 30/30 result but also the 6.7-billion-theorem count derived from the same engine, the authors should provide (a) a complete formal specification of the DSL and its inference rules, (b) a machine-checked verifier or formal certificates for all 30 traces, or (c) a public release of the code and data so that the traces can be replayed and checked. Without one of these, the central claim remains unverified.","section":"Performance on benchmarks; MO-TG-225"},{"comment":"The MO-TG-225 benchmark is self-curated: the text states that its 225 problems were 'selected from our pool of 196 examples used to calculate search statistics.' Because that same pool appears to guide the search that generated the synthetic training data, the benchmark is not independent of the data-generation process. The paper reports no external human baseline or decontamination analysis for this benchmark, yet uses it to claim that TongGeometry 'surpasses the existing state-of-the-art across a broader spectrum of olympiad-level problems.' The authors should release the benchmark, specify exact selection criteria, demonstrate that its problems are disjoint from the training data at the problem level, and ideally compare against additional external benchmarks.","section":"Performance on benchmarks; MO-TG-225"},{"comment":"The supplementary limitation states that 'current models still fall short in sequentially constructing a series of interrelated actions, failing on problems requiring multiple new points to be constructed.' This is in direct tension with the claimed solution of long, multi-step IMO problems, including the two problems flagged as most difficult (IMO 2000 P6 and IMO 2008 P6). The paper should explain how the 30/30 result is consistent with this limitation and should provide the full proof traces for all 30 problems, not just IMO 2024 P4, so that readers can assess the multi-step constructions. This is especially important because long traces are precisely where an unsound heuristic or an invalid derived rule could escape detection.","section":"Supplementary 'Limitation' vs. Table 1"}],"minor_comments":[{"comment":"The caption of Table 1 says 'MO-AG-225' while the text and table body refer to 'MO-TG-225'; this should be corrected.","section":"Figure/Table captions"},{"comment":"The sentence 'AlphaGeometry’s DD+AR approach notably improved upon Wu’s method (10 solves)' is ambiguous because Table 1 lists 'DD+AR (AlphaGeometry)' as 14/30; the paper should clarify whether '10 solves' refers to a baseline in the original AlphaGeometry paper or to the implementation used here.","section":"Performance on benchmarks"},{"comment":"The receipt shown in Figure S13 is administrative evidence of shortlisting, not mathematical evidence; the caption should distinguish between 'accepted as a competition problem' and 'validated as a correct theorem by independent judges.'","section":"Supplementary 'Proof of Proposal Acceptance'"},{"comment":"The phrase '10 theorems were proposed to regional mathematical olympiads' is imprecise: the paper describes 10 problem proposals, of which only three were accepted or shortlisted. The wording should distinguish proposed problems from accepted theorems.","section":"Abstract and main text"}],"recommendation":"major_revision","confidential_remarks":"For the editor: the paper's plausibility is not the main issue; the central obstacle is verifiability. The 30/30 claim and the 6.7-billion-theorem count rest on an unformalized proof calculus and an unreleased implementation. I would support acceptance after the authors supply a formal semantics for the DSL, a verifier or machine-checked certificates, complete proof traces for all 30 IMO-AG-30 problems, and a decontamination analysis for MO-TG-225. This is a substantial but well-scoped revision; I do not view the current deficiencies as unfixable, so I recommend major revision rather than rejection."},"author_rebuttal":null,"desk_editor":{"model":"deepseek-v4-flash","letter":"Colleague,\n\nThe paper is a genuine jump in claimed capability: 30/30 on IMO-AG-30, above the gold-medal average, with three generated problems accepted or shortlisted in real contests. The system is efficient enough to run on a 32-core machine with one GPU, and the ablations suggest the value model actually earns its keep. That is new, and if it holds, it is a milestone.\n\nThe soft spot is exactly where the reader put it: the proof calculus is not specified. The supplementary trace for IMO 2024 P4 uses inference rules like eqangle and eqcircle with no formal semantics, and a rule deriving concyclicity from angle equality is only sound with the right orientation and degeneracy handling. No code, no data, no machine-checked certificates, and only one of thirty traces got a human look. The same engine produces the 6.7B theorem count, so an unsound rule would contaminate both the solve claim and the discovery claim. I don't think the rules are necessarily wrong, but the evidence doesn't establish them.\n\nThe MO-TG-225 benchmark is weaker evidence: it comes from the same seed pool used for training, so I discount that table. The IMO-AG-30 result is the load-bearing one, and there the concern is real but not fatal. The paper would be much stronger with a released verifier or at least a detailed specification of the deductive rules and a soundness argument.\n\nThe authors do state a limitation in the supplementary — the models struggle with sequences of interrelated constructions — and they credit a gold medalist for checking the P4 proof. That is honest. It is not a paper that ignores its own weaknesses.\n\nMy advice: send it to review. A serious referee should look at the rule set line by line and ask for code or certificates, but the claim is important enough to warrant that effort. I'd want the artifacts released before I'd cite the 30/30 as fact, though I'd probably cite the problem-proposing pipeline even now.","headline":"Plausible 30/30 milestone, but the unverified DD rule set is a load-bearing hole that peer review must close.","tokens_in":15634,"tokens_out":2155,"would_cite":false,"duration_ms":18446,"reading_group":"maybe","serious_thinker":"yes","would_accept_peer_review":true},"rs_alignment":null,"lean_confirmation":null,"pith_extraction":{"msc":[],"pacs":[],"model":"deepseek-v4-flash","headline":"The paper claims that TongGeometry, a tree-search system for Euclidean geometry, solves all 30 problems in the IMO-AG-30 benchmark, surpassing the average IMO gold medalist for the first time.","keywords":["automated theorem proving","Euclidean geometry","olympiad geometry","tree search","auxiliary construction","neuro-symbolic system","problem proposing","deductive database"],"falsifier":"Take the 30 IMO-AG-30 proof traces and verify every derived step in an independent formal checker, or have several new gold medalists each review a different subset of the traces; a single unverifiable step would mean the all-30 claim is not established. A cheaper check is to sweep each deductive rule over degenerate configurations, such as collinear points, coincident points, and right angles, and see whether any angle-equality or concyclicity step becomes unsound.","tokens_in":14553,"feed_emoji":"📐","tokens_out":7474,"duration_ms":65807,"temperature":0.7,"pith_summary":"This paper introduces TongGeometry, a Euclidean geometry system that both proposes and solves olympiad-level problems. Its central claim is that TongGeometry solved every geometry problem in the IMO-AG-30 benchmark, becoming the first system to surpass the average gold-medalist score. The same tree-search engine generated billions of provable geometry theorems requiring auxiliary constructions, and it used these as training and guidance data. A sympathetic reader would care because the result suggests an automated system can move beyond solving known problems to discovering new olympiad-style problems, some of which were accepted into real competitions.","feed_headline":"Geometry engine solves all 30 IMO problems, beats gold medalists","feed_subtitle":"A tree-search engine proves every problem in the IMO-AG-30 benchmark in under 38 minutes on one consumer GPU.","key_machinery":"The central object is a finite tree over synthetic Euclidean configurations, paired with a deductive database of full-angle geometry rules. Forward chaining over these rules produces human-readable proofs, while backward tracing from proved configurations proposes new theorems. The search is guided by an actor-critic-style pair of language models: a policy model that suggests auxiliary points and lines, and a value model that estimates how many proof steps remain. This learned guidance is what raises the system from 18 of 30 solved problems with the deductive backend alone to 30 of 30 with the full neuro-symbolic pipeline.","core_discovery":"TongGeometry combines a deductive database of synthetic geometry rules with two fine-tuned language models that guide tree search: one proposes auxiliary constructions and the other estimates the remaining proof length. Within 30 days of search on 10,368 parallel CPU cores, the system traversed 143,379,886 unique paths, inferred over 1.85 billion unique states, and filtered these into 6,688,310,403 provable problems requiring auxiliary constructions, of which 4,096,680,574 are symmetric. Guided by the learned models, the system solved all 30 problems in IMO-AG-30 in at most 38 minutes per problem on a consumer-grade machine, surpassing the average gold-medalist score of 25.9 out of 30. On a broader benchmark of 225 olympiad problems, it solved 183. The paper also reports that three of its automatically proposed problems were selected for or shortlisted in regional olympiad competitions.","pith_inferences":["If the underlying rule set is sound, the 6.7-billion-theorem corpus is itself a transferable asset that could train future geometry systems without any human-written proofs, with the symmetry-filtered subset potentially biasing training toward more elegant problems.","The same actor-critic tree-search recipe may transfer to other synthetic domains with a deductive rule set, such as algebraic inequalities or combinatorial geometry, although the auxiliary-construction policy would need to be re-learned for each domain.","A testable extension is to run the unmodified system on the next several years of IMO geometry problems before official solutions appear and have independent gold medalists review every trace; this would measure whether the 30-of-30 result generalizes beyond a fixed benchmark.","The paper's 'coach' analogy implies a longer-term experiment: use the selection rubrics to generate a steady stream of olympiad proposals over several seasons and track their acceptance rate, which would test whether the proposing pipeline reliably produces competition-quality problems."],"forward_implications":["If the central claim holds, a consumer-grade machine with 32 CPU cores and a single GPU can solve every IMO geometry problem in the benchmark within 38 minutes, making olympiad-level geometry reasoning widely accessible.","The system solved 183 of 225 problems in the broader MO-TG-225 dataset, surpassing the previous state-of-the-art system's 102 solves.","The search produced 6.7 billion provable theorems requiring auxiliary constructions, including 4.1 billion with geometric symmetry, a synthetic corpus far larger than previous collections.","Three of the system's automatically proposed problems were selected for or shortlisted in real regional olympiad competitions, demonstrating that the proposing pipeline can produce problems humans judge suitable.","The value heuristic improved solve rates by 7.1 percentage points on IMO-AG-30 and 3.4 percentage points on MO-TG-225 over a policy-only version, showing that learned guidance contributes beyond raw search."],"supporting_citations":[{"why":"Supplies the IMO-AG-30 benchmark and the baseline performance numbers the paper compares against.","marker":"[2]"},{"why":"Provides the earlier problem-proposing approach and the rubric methodology adapted for selecting TongGeometry's proposals.","marker":"[14]"},{"why":"Base model family for the fine-tuned policy and value language models that guide tree search.","marker":"[15]"},{"why":"Informs the compute budget and scaling used to train the language-model guides.","marker":"[16]"},{"why":"The deductive database technique that TongGeometry's forward-chaining backend is built on.","marker":"[26]"},{"why":"Supplies the full-angle proof rules used by the deductive database.","marker":"[28]"},{"why":"Official solutions to IMO 2024 P4, used to confirm that TongGeometry's auxiliary point matches the human construction.","marker":"[21]"}],"fun_headline_variants":["Geometry AI beats gold medalists on all 30 IMO problems","Tree-search engine solves every IMO geometry problem, outperforms gold","AI discovers 6.7B geometry theorems and solves all IMO-AG-30","Coach-like AI invents olympiad problems, solves all IMO-AG-30"],"cache_read_input_tokens":3200,"weakest_assumption_plain":"The load-bearing premise is that every rule in the deductive database is sound for every non-degenerate configuration the search visits; if any rule silently assumes an orientation or misses a degenerate case, a proof that looks correct could be invalid, and the paper does not formally verify the rules or most of the proof traces.","fun_headline_variants_meta":{"raw":{"variants":["Geometry AI beats gold medalists on all 30 IMO problems","Tree-search engine solves every IMO geometry problem, outperforms gold","AI discovers 6.7B geometry theorems and solves all IMO-AG-30","Coach-like AI invents olympiad problems, solves all IMO-AG-30"]},"model":"deepseek-v4-flash","effort":"low","cost_usd":0.000522,"raw_usage":{"total_tokens":2550,"prompt_tokens":994,"completion_tokens":1556,"prompt_tokens_details":{"cached_tokens":384},"prompt_cache_hit_tokens":384,"prompt_cache_miss_tokens":610,"completion_tokens_details":{"reasoning_tokens":1472}},"tokens_in":610,"tokens_out":1556,"duration_ms":11764,"temperature":1.0,"reasoning_tokens":1472,"cache_read_input_tokens":384,"cache_creation_input_tokens":0},"cache_creation_input_tokens":0},"created_at":"2026-08-11T15:43:38.304550+00:00","model_set":{"reader":"deepseek-v4-flash"},"falsifier":"Take the 30 IMO-AG-30 proof traces and verify every derived step in an independent formal checker, or have several new gold medalists each review a different subset of the traces; a single unverifiable step would mean the all-30 claim is not established. A cheaper check is to sweep each deductive rule over degenerate configurations, such as collinear points, coincident points, and right angles, and see whether any angle-equality or concyclicity step becomes unsound.","supporting_citations":[],"review_version":1}