Pith. sign in

REVIEW 3 major objections 4 minor 1 cited by

Proposing and solving olympiad geometry with guided tree search

T0 review · 3 major / 4 minor · reviewed 2026-08-11 · deepseek-v4-flash

Challenge this review Re-run · record.json Download PDF Read on arXiv ↗ Review JSON

Pith's one-line read 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.

desk verdict Plausible 30/30 milestone, but the unverified DD rule set is a load-bearing hole that peer review must close. read the letter →

arxiv 2412.10673 v1 pith:A3TEI4SJ submitted 2024-12-14 cs.AI cs.LG

Chi Zhang , Jiajun Song , Siyu Li , Yitao Liang , Yuxi Ma , Wei Wang , Yixin Zhu , Song-Chun Zhu This is my paper · ORCID
classification cs.AIcs.LG
keywords automatedtheoremprovingEuclideangeometryolympiadtreesearchauxiliaryconstructionneuro-symbolicsystemproblemproposingdeductivedatabase
verification ladder T0 review T1 audit T2 compute T3 formal

The pith

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The reading

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.

What carries the argument

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.

What would settle it

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.

Watch

Extended reading notes

Core claim

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.

Load-bearing premise

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.

Editorial extensions

If this is right

  • 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.

Reading between the lines

Editorial extensions of the paper, not claims the author makes directly.

  • 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.
Share X Bluesky LinkedIn Reddit HN

Signed reviews

No signed human review yet.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, and a circularity audit.

Referee Report

3 major / 4 minor

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.

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 (3)
  1. [Performance on benchmarks; MO-TG-225] 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.
  2. [Performance on benchmarks; MO-TG-225] 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.
  3. [Supplementary 'Limitation' vs. Table 1] 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.
minor comments (4)
  1. [Figure/Table captions] The caption of Table 1 says 'MO-AG-225' while the text and table body refer to 'MO-TG-225'; this should be corrected.
  2. [Performance on benchmarks] 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.
  3. [Supplementary 'Proof of Proposal Acceptance'] 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.'
  4. [Abstract and main text] 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.

Circularity Check

0 steps flagged · score 0.0 of 10

No circular derivation found: the headline 30/30 result is an external benchmark evaluation whose proofs are produced by a separate symbolic engine, and the paper contains no load-bearing self-citation or fitted-input-as-prediction reduction.

full rationale

The claimed derivation chain is empirical rather than deductive. TongGeometry's central claim is that its tree-search engine, guided by fine-tuned LLMs, solves all 30 problems in the external IMO-AG-30 benchmark. The benchmarks and human baselines come from prior work (AlphaGeometry), not from TongGeometry's own fitted values; the final solved traces are attributed to the symbolic deductive-database backend rather than to the neural models themselves. The policy and value models are trained on synthetic data produced by the same geometry engine, and the MO-TG-225 benchmark is drawn from the same 196-problem pool used to compute search statistics; these are self-referential training/evaluation choices that merit a data-leakage or generalization caveat, but they do not make any particular 'solve' equivalent to an input by construction. The IMO-2024-P4 trace is a sequence of standard inference-rule applications (contri, simtri, eqangle, eqcircle, eqline, midp), and deriving a circle from equal angles is a classical geometry fact, not a renaming of the target. The paper's cited limitations—no released code or verifier, no formal soundness proof for the custom rule set, and only one of thirty traces human-checked—are verification gaps that could invalidate the 30/30 claim if a rule is unsound, but they are not circularity: an unverified proof checker is not the same as a conclusion that is its own premise. No self-citation chain, uniqueness theorem, or ansatz-smuggling-via-citation appears in the paper; the references to prior work (AlphaGeometry, GeoGen) are comparisons or methodology inspirations. Accordingly, no circular step is exhibited, and the appropriate score is 0.

Assumptions & free parameters 2 free parameters · 4 assumptions · 0 invented entities

The central claims rest on the soundness of the system's inference rules, the fidelity of problem translation, the accuracy of prior human baselines, and the absence of training/test overlap. These are domain assumptions rather than free numerical parameters; the only fitted quantities are the undisclosed neural model weights and rubric thresholds. No new mathematical or physical entities are postulated; the auxiliary constructions are existing Euclidean objects such as circumcenters, projections and reflections.

free parameters (2)
  • Policy and value model weights = Not disclosed
    The two fine-tuned LLMs that guide auxiliary construction and estimate remaining proof steps are fitted to synthetic search traces; without released weights the guidance cannot be reproduced or audited.
  • Rubric thresholds for olympiad-problem selection = Not disclosed
    The criteria used to choose 10 proposals from billions of generated problems are described qualitatively; the actual scoring thresholds are not specified, so the proposal-selection process is not reproducible.
assumptions (4)
  • domain assumption Soundness of the deductive database rules
    The entire proof engine derives facts such as congruence, similarity and concyclicity from angle and ratio rules; the paper provides no formal verification that these rules are sound for all non-degenerate configurations, including orientation and collinearity edge cases. Invoked in Table 1 and the IMO 2024 P4 proof traces.
  • domain assumption Faithful translation of olympiad problems into TongGeometry's domain-specific language
    The 30/30 and 183/225 solve counts depend on the correctness of translating natural-language geometry problems into the DSL; translation errors could make a solved problem different from the original. Invoked in the benchmark evaluation section.
  • domain assumption Human baseline scores on IMO-AG-30 are accurate
    The 'outperforming gold medalists' claim compares TongGeometry's 30/30 with the 25.9/30 average gold medalist score reported in AlphaGeometry (ref 2) and assumes those human scores were obtained under comparable conditions on the same translated benchmark.
  • domain assumption MO-TG-225 test problems do not overlap with training data
    The authors state none of the 225 problems appear in the training dataset, but without released datasets this cannot be verified; since the benchmark is drawn from the same 196-problem seed pool used to guide search, the separation is a load-bearing assumption.

how reviews work

0 comments
Cite this review

Pith. "Pith review of Proposing and solving olympiad geometry with guided tree search." pith.science (2026). https://pith.science/paper/A3TEI4SJ

@misc{pith2026241210673,
  author       = {Pith},
  title        = {Pith review of: Proposing and solving olympiad geometry with guided tree search},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/A3TEI4SJ}},
  note         = {Machine review of arXiv:2412.10673}
}
read the original abstract

Mathematics olympiads are prestigious competitions, with problem proposing and solving highly honored. Building artificial intelligence that proposes and solves olympiads presents an unresolved challenge in automated theorem discovery and proving, especially in geometry for its combination of numerical and spatial elements. We introduce TongGeometry, a Euclidean geometry system supporting tree-search-based guided problem proposing and solving. The efficient geometry system establishes the most extensive repository of geometry theorems to date: within the same computational budget as the existing state-of-the-art, TongGeometry discovers 6.7 billion geometry theorems requiring auxiliary constructions, including 4.1 billion exhibiting geometric symmetry. Among them, 10 theorems were proposed to regional mathematical olympiads with 3 of TongGeometry's proposals selected in real competitions, earning spots in a national team qualifying exam or a top civil olympiad in China and the US. Guided by fine-tuned large language models, TongGeometry solved all International Mathematical Olympiad geometry in IMO-AG-30, outperforming gold medalists for the first time. It also surpasses the existing state-of-the-art across a broader spectrum of olympiad-level problems. The full capabilities of the system can be utilized on a consumer-grade machine, making the model more accessible and fostering widespread democratization of its use. By analogy, unlike existing systems that merely solve problems like students, TongGeometry acts like a geometry coach, discovering, presenting, and proving theorems.

Discussion (0). Continue with ORCID to comment.

Forward citations

Cited by 1 Pith paper

Reviewed papers in the Pith corpus that reference this work. Sorted by Pith novelty score. Full citation record

  1. Seed-Prover: Deep and Broad Reasoning for Automated Theorem Proving

    cs.AI 2025-07 conditional novelty 6.0 of 10

    Seed-Prover and Seed-Geometry prove 121 of 155 formalized past IMO problems, reach 99.6% on MiniF2F-test, and solve 5 of 6 IMO 2025 problems after the competition deadline.

Reference graph

Works this paper leans on

138 extracted references · 67 canonical work pages · cited by 1 Pith paper

  1. [25]

    S.-C. Chou, W. F. Schelter, Proving geometry theorems with rewrite rules.Journal of Automated Reasoning 2, 253–273 (1986). 12

    1986

  2. [27]

    S.-C. Chou, X. Gao, J.-Z. Zhang, Machine proofs in geometry: Automated production of readable proofs for geometry theorems, vol. 6 (World Scientific) (1994)

    1994

  3. [36]

    De Moura, N

    L. De Moura, N. Bjørner, Z3: An efficient SMT solver, in International conference on Tools and Algorithms for the Construction and Analysis of Systems (Springer) (2008), pp. 337–340

    2008

  4. [37]

    LeCun, Y

    Y. LeCun, Y. Bengio, G. Hinton, Deep learning. nature 521 (7553), 436–444 (2015)

    2015

  5. [1]

    Selsam, et al., IMO Grand Challenge

    D. Selsam, et al., IMO Grand Challenge. URL https://imo-grand-challenge.github.io(2020)

    2020

  6. [2]

    T. H. Trinh, Y. Wu, Q. V. Le, H. He, T. Luong, Solving olympiad geometry without human demonstrations. Nature 625 (7995), 476–482 (2024)

    2024

  7. [3]

    S. Polu, I. Sutskever, Generative language modeling for automated theorem proving. arXiv preprint arXiv:2009.03393 (2020)

    arXiv 2020

  8. [4]

    Zheng, J

    K. Zheng, J. M. Han, S. Polu, Minif2f: a cross-system benchmark for formal olympiad-level mathematics. arXiv preprint arXiv:2109.00110 (2021)

    arXiv 2021

Show all 138 references
  1. [5]

    Polu, et al

    S. Polu, et al. , Formal mathematics statement curriculum learning. arXiv preprint arXiv:2202.01344 (2022)

    2022 arXiv

  2. [6]

    Lample, et al., Hypertree proof search for neural theorem proving

    G. Lample, et al., Hypertree proof search for neural theorem proving. Advances in neural information processing systems 35, 26337–26349 (2022)

    2022

  3. [7]

    Achiam, et al., Gpt-4 technical report

    J. Achiam, et al., Gpt-4 technical report. arXiv preprint arXiv:2303.08774 (2023)

    2023 arXiv

  4. [8]

    Touvron, et al

    H. Touvron, et al. , Llama: Open and efficient foundation language models. arXiv preprint arXiv:2302.13971 (2023)

    2023 arXiv

  5. [9]

    W. W. R. Ball, A short account of the history of mathematics (Courier Corporation) (1960)

    1960

  6. [10]

    Mari ´c, et al., Formalizing IMO problems and solutions in Isabelle/HOL

    F. Mari ´c, et al., Formalizing IMO problems and solutions in Isabelle/HOL. arXiv preprint arXiv:2010.16015 (2020)

    2020

  7. [11]

    L. d. Moura, S. Ullrich, The Lean 4 theorem prover and programming language, in Automated Deduction–CADE 28: 28th International Conference on Automated Deduction, Virtual Event, July 12–15, 2021, Proceedings 28 (Springer) (2021), pp. 625–635

    2021

  8. [12]

    Chou, X.-S

    S.-C. Chou, X.-S. Gao, J.-Z. Zhang, An introduction to geometry expert, in Automated Deduction—Cade-13: 13th International Conference on Automated Deduction New Brunswick, NJ, USA, July 30–August 3, 1996 Proceedings 13 (Springer) (1996), pp. 235–239. 11

    1996

  9. [13]

    Sangwin, A brief review of GeoGebra: dynamic mathematics

    C. Sangwin, A brief review of GeoGebra: dynamic mathematics. MSor Connections 7 (2), 36 (2007)

    2007

  10. [14]

    P. Bak, R. S. Kraj ˇci, M. M. Rol ´ınek, Automated generation of planar geometry Olympiad problems, Ph.D. thesis, Master Thesis (2020)

    2020

  11. [15]

    Guo, et al., DeepSeek-Coder: When the Large Language Model Meets Programming–The Rise of Code Intelligence

    D. Guo, et al., DeepSeek-Coder: When the Large Language Model Meets Programming–The Rise of Code Intelligence. arXiv preprint arXiv:2401.14196 (2024)

    2024 arXiv

  12. [16]

    Hoffmann, et al

    J. Hoffmann, et al. , Training compute-optimal large language models. arXiv preprint arXiv:2203.15556 (2022)

    2022 arXiv

  13. [17]

    J. S. Mackay, History of the Nine-point Circle. Proceedings of the Edinburgh Mathematical Society 11, 19–57 (1892)

  14. [18]

    Chen, Euclidean geometry in mathematical olympiads , vol

    E. Chen, Euclidean geometry in mathematical olympiads , vol. 27 (American Mathematical Soc.) (2021)

    2021

  15. [19]

    Chen, A Guessing Game: Mixtilinear Incircles

    E. Chen, A Guessing Game: Mixtilinear Incircles. URL https://web.evanchen.cc/handouts/Mixt-GeoGuessr/Mixt-GeoGuessr.pdf (2015)

    2015

  16. [20]

    Chen, The Incenter/Excenter Lemma.URL https://web.evanchen.cc/handouts/Fact5/Fact5.pdf (2016)

    E. Chen, The Incenter/Excenter Lemma.URL https://web.evanchen.cc/handouts/Fact5/Fact5.pdf (2016)

    2016

  17. [21]

    T. O. Committee, the Problem Selection Committee of IMO 2024, 65th International Mathe- matical Olympiad Problems with Solutions. URL https://www.imo2024.uk/solutions (2024)

    2024

  18. [22]

    Wu, On the decision problem and the mechanization of theorem-proving in elementary geometry, in Selected Works Of Wen-Tsun Wu(World Scientific), pp

    W.-t. Wu, On the decision problem and the mechanization of theorem-proving in elementary geometry, in Selected Works Of Wen-Tsun Wu(World Scientific), pp. 117–138 (2008)

    2008

  19. [23]

    Chou, Mechanical geometry theorem proving(Springer) (1988)

    S.-C. Chou, Mechanical geometry theorem proving(Springer) (1988)

    1988

  20. [24]

    Chou, Proving elementary geometry theorems using Wu’s algorithm, Ph.D

    S.-C. Chou, Proving elementary geometry theorems using Wu’s algorithm, Ph.D. thesis, Uni- versity of Texas at Austin (1984)

    1984

  21. [26]

    Chou, X.-S

    S.-C. Chou, X.-S. Gao, J.-Z. Zhang, A deductive database approach to automated geometry theorem proving and discovering. Journal of Automated Reasoning 25 (3), 219–246 (2000)

    2000

  22. [28]

    Chou, X.-S

    S.-C. Chou, X.-S. Gao, J.-Z. Zhang, Automated generation of readable proofs with geometric invariants: II. Theorem proving with full-angles. Journal of Automated Reasoning 17 (3), 349–370 (1996)

    1996

  23. [29]

    Hilbert, The foundations of geometry (Open court publishing Company) (1902)

    D. Hilbert, The foundations of geometry (Open court publishing Company) (1902)

    1902

  24. [30]

    AlphaGeometry’s DD+AR approach notably improved upon Wu’s method (10 solves), yet its symbolic reasoning engine remains both redundant and suboptimal

    While the latest reasoning-enhanced language model of o1 achieved impressive results on a range of tasks, we observed that large language models still struggle with rigorous mathematical 5 reasoning in geometry, often generating proofs with erroneous logics and hallucinated in...

    2000

  25. [31]

    Tarski, A decision method for elementary algebra and geometry, in Quantifier elimination and cylindrical algebraic decomposition (Springer), pp

    A. Tarski, A decision method for elementary algebra and geometry, in Quantifier elimination and cylindrical algebraic decomposition (Springer), pp. 24–84 (1998)

    1998

  26. [32]

    Matsuda, K

    N. Matsuda, K. Vanlehn, Gramy: A geometry theorem prover capable of construction.Journal of Automated Reasoning 32, 3–33 (2004)

    2004

  27. [33]

    K. Wang, Z. Su, Automated geometry theorem proving for human-readable proofs, in Twenty- Fourth International Joint Conference on Artificial Intelligence(2015)

    2015

  28. [34]

    Schulz, E–a brainiac theorem prover

    S. Schulz, E–a brainiac theorem prover. Ai Communications 15 (2-3), 111–126 (2002)

    2002

  29. [35]

    Weidenbach, et al., SPASS Version 3.5, inAutomated Deduction–CADE-22: 22nd Interna- tional Conference on Automated Deduction, Montreal, Canada, August 2-7, 2009

    C. Weidenbach, et al., SPASS Version 3.5, inAutomated Deduction–CADE-22: 22nd Interna- tional Conference on Automated Deduction, Montreal, Canada, August 2-7, 2009. Proceedings 22 (Springer) (2009), pp. 140–145

    2009

  30. [38]

    S. Loos, G. Irving, C. Szegedy, C. Kaliszyk, Deep network guided proof search.arXiv preprint arXiv:1701.06972 (2017)

    2017 arXiv

  31. [39]

    C. Wei, M. Sun, W. Wang, Proving Olympiad Algebraic Inequalities without Human Demon- strations. arXiv preprint arXiv:2406.14219 (2024). 13

    2024 arXiv

  32. [40]

    Silver, et al., Mastering the game of Go with deep neural networks and tree search

    D. Silver, et al., Mastering the game of Go with deep neural networks and tree search. nature 529 (7587), 484–489 (2016)

    2016

  33. [41]

    Silver, et al., Mastering the game of go without human knowledge

    D. Silver, et al., Mastering the game of go without human knowledge. nature 550 (7676), 354–359 (2017)

    2017

  34. [42]

    Silver, et al., A general reinforcement learning algorithm that masters chess, shogi, and Go through self-play

    D. Silver, et al., A general reinforcement learning algorithm that masters chess, shogi, and Go through self-play. Science 362 (6419), 1140–1144 (2018)

    2018

  35. [43]

    Megill, D

    N. Megill, D. A. Wheeler, Metamath: a computer language for mathematical proofs (Lulu. com) (2019)

    2019

  36. [44]

    Ayg¨ un,et al., Proving theorems using incremental learning and hindsight experience replay, in International Conference on Machine Learning (PMLR) (2022), pp

    E. Ayg¨ un,et al., Proving theorems using incremental learning and hindsight experience replay, in International Conference on Machine Learning (PMLR) (2022), pp. 1198–1210

    2022

  37. [45]

    Firoiu, et al

    V. Firoiu, et al. , Training a first-order theorem prover from synthetic data. arXiv preprint arXiv:2103.03798 (2021)

    2021 arXiv

  38. [46]

    Liu, et al., Tinygsm: achieving¿ 80% on gsm8k with small language models.arXiv preprint arXiv:2312.09241 (2023)

    B. Liu, et al., Tinygsm: achieving¿ 80% on gsm8k with small language models.arXiv preprint arXiv:2312.09241 (2023)

    2023 arXiv

  39. [47]

    Wu, et al., Autoformalization with large language models

    Y. Wu, et al., Autoformalization with large language models. Advances in Neural Information Processing Systems 35, 32353–32368 (2022)

    2022

  40. [48]

    Uesato, et al., Solving math word problems with process-and outcome-based feedback.arXiv preprint arXiv:2211.14275 (2022)

    J. Uesato, et al., Solving math word problems with process-and outcome-based feedback.arXiv preprint arXiv:2211.14275 (2022)

    2022 arXiv

  41. [49]

    Lightman, et al., Let’s verify step by step.arXiv preprint arXiv:2305.20050 (2023)

    H. Lightman, et al., Let’s verify step by step.arXiv preprint arXiv:2305.20050 (2023). Acknowledgments This project is a two-year long collaboration between Beijing Institute for General Artificial Intelli- gence and Peking University. Along the journey, we would like to thank...

    2023 arXiv

  42. [50]

    contri (AFI, ZfI) because eqangle (AIF, ZIf)[0], cong (FI, If)[0], cong (AI, IZ)[0]

  43. [51]

    contri (AEI, ZeI) because eqangle (AIE, ZIe)[0], cong (EI, Ie)[0], cong (AI, IZ)[0]

  44. [52]

    simtri (EFe, ZfI) because eqangle (EeF, ZIf)[0], eqratio (Ee, IZ, Fe, If)[0]

  45. [53]

    simtri (EFe, ZeI) because eqangle (EeF, eIZ)[0], eqratio (Ee, IZ, Fe, Ie)[0]

  46. [54]

    simtri (ACZ, AKI) because eqangle (CAZ, KAI)[0], eqratio (AC, AK, AZ, AI)[0]

  47. [55]

    simtri (ABZ, ALI) because eqangle (BAZ, LAI)[0], eqratio (AB, AL, AZ, AI)[0]

  48. [56]

    eqangle (AFI, ZfI) because contri (AFI, ZfI)[1]

  49. [57]

    eqangle (AEI, ZeI) because contri (AEI, ZeI)[2]

  50. [58]

    eqangle (FEe, fZI) because simtri (EFe, ZfI)[3]

  51. [59]

    eqangle (FEe, IZe) because simtri (EFe, ZeI)[4]

  52. [60]

    eqangle (AIK, AZC) because simtri (ACZ, AKI)[5]

  53. [61]

    eqangle (AIL, AZB) because simtri (ABZ, ALI)[6]

  54. [62]

    eqangle (IFf, YfZ) because eqangle (AFI, ZfI)[7], eqangle (AFf, YfI)[0]

  55. [63]

    eqangle (IEe, XeZ) because eqangle (AEI, ZeI)[8], eqangle (AEe, XeI)[0]

  56. [64]

    eqangle (AZf, PCY) because eqangle (FEe, YCP)[0], eqangle (FEe, fZI)[9], eqangle (AZf, IZf)[0]

  57. [65]

    eqangle (AZe, PBX) because eqangle (AZe, IZe)[0], eqangle (FEe, IZe)[10], eqangle (FEe, PBX)[0]

  58. [66]

    eqangle (AIK, PZC) because eqangle (AIK, AZC)[11], eqangle (AZC, PZC)[0]

  59. [67]

    eqangle (AIL, PZB) because eqangle (AIL, AZB)[12], eqangle (AZB, PZB)[0]

  60. [68]

    eqline (Yf, Zf) because eqangle (IFf, YfZ)[13], eqline (FI, Ff)[0]

  61. [69]

    eqline (Xe, Ze) because eqangle (IEe, XeZ)[14], eqline (EI, Ee)[0]

  62. [70]

    eqangle (PCY, PZY) because eqangle (AZY, PZY)[0], eqangle (AZY, AZf)[19], eqangle (AZf, PCY)[15]

  63. [71]

    eqangle (CYf, XYZ) because eqangle (AYZ, AYf)[19], eqangle (AYC, AYX)[0]

  64. [72]

    eqangle (PBX, PZX) because eqangle (AZX, PZX)[0], eqangle (AZX, AZe)[20], eqangle (AZe, PBX)[16]

  65. [73]

    eqangle (BXe, YXZ) because eqangle (AXZ, AXe)[20], eqangle (AXB, AXY)[0]

  66. [74]

    eqcircle (None, CPY, None, PYZ) because eqangle (PCY, PZY)[21]

  67. [75]

    eqangle (CYP, XYP) because eqangle (PYZ, PYf)[19], eqangle (CYf, XYZ)[22] S5

  68. [76]

    eqcircle (None, BPX, None, PXZ) because eqangle (PBX, PZX)[23]

  69. [77]

    eqangle (BXP, YXP) because eqangle (PXZ, PXe)[20], eqangle (BXe, YXZ)[24]

  70. [78]

    eqangle (CYP, CZP) because eqcircle (None, CPY, None, PYZ)[25]

  71. [79]

    eqangle (BXP, BZP) because eqcircle (None, BPX, None, PXZ)[27]

  72. [80]

    eqangle (AIK, PYX) because eqangle (AIK, PZC)[17], eqangle (CYP, CZP)[29], eqangle (CYP, XYP)[26]

  73. [81]

    eqangle (AIL, PXY) because eqangle (AIL, PZB)[18], eqangle (BXP, BZP)[30], eqangle (BXP, YXP)[28]

  74. [82]

    eqangle (KIL, XPY) because eqangle (AIK, PYX)[31], eqangle (AIL, PXY)[32] Z = IntersectLineLine(X, e, Y, f)

  75. [83]

    cong (EF, ef) because contri (EFI, efI)[0]

  76. [84]

    cong (Pe, Pf) because contri (IPe, IPf)[0]

  77. [85]

    cong (Ae, Af) because contri (AIe, AIf)[0]

  78. [86]

    simtri (AEF, Zfe) because eqangle (AFE, feZ)[0], eqangle (AEF, efZ)[0]

  79. [87]

    eqcircle (None, IZe, None, IZf) because eqangle (IeZ, IfZ)[0]

  80. [88]

    eqratio (AE, Zf, EF, ef) because simtri (AEF, Zfe)[4]

  81. [89]

    eqangle (ZIe, Zfe) because eqcircle (None, IZe, None, IZf)[5]

  82. [90]

    eqangle (IZf, Ief) because eqcircle (None, IZe, None, IZf)[5]

  83. [91]

    contri (PZe, PZf) because cong (Ze, Zf)[0], cong (Pe, Pf)[2]

  84. [92]

    contri (AZe, AZf) because cong (Ze, Zf)[0], cong (Ae, Af)[3]

  85. [93]

    cong (AE, Zf) because eqratio (AE, Zf, EF, ef)[6], cong (EF, ef)[1]

  86. [94]

    eqangle (AIZ, YfZ) because eqangle (ZIe, Zfe)[7], eqangle (AIe, Yfe)[0]

  87. [95]

    eqangle (PIZ, YfZ) because eqangle (ZIe, Zfe)[7], eqangle (PIe, Yfe)[0]

  88. [96]

    eqangle (IAL, IZY) because eqangle (IAL, Ief)[0], eqangle (IZf, Ief)[8], eqangle (IZY, IZf)[0]

  89. [97]

    eqangle (IZY, XBP) because eqangle (Ief, XBP)[0], eqangle (IZf, Ief)[8], eqangle (IZY, IZf)[0]

  90. [98]

    eqangle (IAK, YZI) because eqangle (IAK, feI)[0], eqangle (IZf, Ief)[8], eqangle (IZY, IZf)[0]

  91. [99]

    eqangle (IZY, PCY) because eqangle (Ief, PCY)[0], eqangle (IZf, Ief)[8], eqangle (IZY, IZf)[0]

  92. [100]

    eqangle (PZe, fZP) because contri (PZe, PZf)[9]

  93. [101]

    eqangle (AZe, fZA) because contri (AZe, AZf)[10]

  94. [102]

    contri (AEI, ZfI) because cong (AE, Zf)[11], perp (AEI)[0], perp (IfZ)[0], cong (EI, If)[0]

  95. [103]

    eqline (AI, IZ) because eqangle (AIZ, YfZ)[12], eqline (Yf, Zf)[0]

  96. [104]

    eqline (IP, IZ) because eqangle (PIZ, YfZ)[13], eqline (Yf, Zf)[0]

  97. [105]

    eqangle (PZX, YZP) because eqangle (PZX, PZe)[0], eqangle (PZe, fZP)[18], eqangle (PZY, PZf)[0]

  98. [106]

    eqangle (AZP, PZA) because eqangle (PZe, fZP)[18], eqangle (AZe, fZA)[19]

  99. [107]

    eqangle (AZY, CAZ) because eqangle (AZe, ZAC)[0], eqangle (AZe, fZA)[19], eqangle (AZY, AZf)[0]

  100. [108]

    cong (AI, IZ) because contri (AEI, ZfI)[20]

  101. [109]

    midp (I, AZ) because cong (AI, IZ)[26], eqline (AI, IZ)[21]

  102. [110]

    eqratio (AB, AL, AZ, AI) because midp (I, AZ)[27], midp (L, AB)[0]

  103. [111]

    eqratio (AC, AK, AZ, AI) because midp (I, AZ)[27], midp (K, AC)[0]

  104. [112]

    eqangle (BAZ, LAI) because eqangle (AZY, ZAB)[0], eqangle (AZY, IZY)[21], eqangle (IAL, IZY)[14]

  105. [113]

    eqangle (CAZ, KAI) because eqangle (AZY, CAZ)[25], eqangle (AZY, IZY)[21], eqangle (IAK, YZI)[16]

  106. [114]

    eqangle (PBX, PZX) because eqangle (IZY, XBP)[15], eqangle (IZY, PZY)[22], eqangle (PZX, YZP)[23]

  107. [115]

    eqangle (PCY, PZY) because eqangle (IZY, PCY)[17], eqangle (IZY, PZY)[22]

  108. [116]

    simtri (ABZ, ALI) because eqratio (AB, AL, AZ, AI)[28], eqangle (BAZ, LAI)[30]

  109. [117]

    simtri (ACZ, AKI) because eqratio (AC, AK, AZ, AI)[29], eqangle (CAZ, KAI)[31]

  110. [118]

    eqcircle (None, BPX, None, PXZ) because eqangle (PBX, PZX)[32]

  111. [119]

    eqcircle (None, CPY, None, PYZ) because eqangle (PCY, PZY)[33] S6

  112. [120]

    eqangle (AIL, AZB) because simtri (ABZ, ALI)[34]

  113. [121]

    eqangle (AIK, AZC) because simtri (ACZ, AKI)[35]

  114. [122]

    eqangle (BXP, BZP) because eqcircle (None, BPX, None, PXZ)[36]

  115. [123]

    eqangle (CYP, CZP) because eqcircle (None, CPY, None, PYZ)[37]

  116. [124]

    eqangle (AZB, PXY) because eqangle (AZB, PZB)[24], eqangle (BXP, BZP)[40], eqangle (BXP, YXP)[0]

  117. [125]

    eqangle (AZC, PYX) because eqangle (AZC, PZC)[24], eqangle (CYP, CZP)[41], eqangle (CYP, XYP)[0]

  118. [126]

    eqangle (AIL, PXY) because eqangle (AIL, AZB)[38], eqangle (AZB, PXY)[42]

  119. [127]

    eqangle (AIK, PYX) because eqangle (AIK, AZC)[39], eqangle (AZC, PYX)[43]

  120. [128]

    eqangle (KIL, XPY) because eqangle (AIL, PXY)[44], eqangle (AIK, PYX)[45] TongGeometry Proposals to 2024 USEMO

    2024

  121. [129]

    A circumcircle centered at𝐼 passes through△𝐷𝐸𝐹 .𝐽 is the foot of𝐼 to𝐶𝐷

    Figure S2: Let△𝐴𝐵𝐶 be an acute-angled triangle,𝐷 be its incenter,𝐸 be its𝐵-excenter and 𝐹 its𝐴-excenter.𝐺 is the center of⊙(𝐶𝐵𝐸) and𝐻 is the center of⊙(𝐴𝐶𝐹). A circumcircle centered at𝐼 passes through△𝐷𝐸𝐹 .𝐽 is the foot of𝐼 to𝐶𝐷 . Prove𝐺𝐻𝐼𝐽 are concyclic

  122. [130]

    Let 𝐸 be the circumcenter of⊙(𝐴𝐶𝐷) and𝐹 be that of⊙(𝐵𝐶𝐷)

    Figure S3: Let △𝐴𝐵𝐶 be an acute-angled triangle and 𝐷 be its incenter. Let 𝐸 be the circumcenter of⊙(𝐴𝐶𝐷) and𝐹 be that of⊙(𝐵𝐶𝐷). Project 𝐷 to𝐶𝐸 to get𝐺 and project 𝐷 to𝐶𝐹 to get 𝐻. Denote the other intersection of 𝐸𝐶 with⊙(𝐵𝐶𝐷) as 𝐼 and that of 𝐹𝐶 with⊙(𝐴𝐶𝐷) as𝐽. 𝐼𝐷 and𝐽𝐷 inte...

  123. [131]

    𝐸 is on 𝐶𝐷 such that ∠𝐸𝐴𝐶 is a right angle.𝐹 is on𝐶𝐷 such that ∠𝐹𝐵𝐶 is a right angle

    Figure S4: Let △𝐴𝐵𝐶 be an acute-angled triangle and 𝐷 be its incenter. 𝐸 is on 𝐶𝐷 such that ∠𝐸𝐴𝐶 is a right angle.𝐹 is on𝐶𝐷 such that ∠𝐹𝐵𝐶 is a right angle. The circumcircle of △𝐴𝐸𝐷 meets𝐵𝐶 again at𝐼 and the circumcircle of△𝐵𝐹𝐷 meets𝐵𝐶 again at𝐽. Let𝐾 be the midpoint of𝐼𝐽 . De...

  124. [132]

    The projection of𝐷 on𝐴𝐵, denoted as𝐸, forms two circumcircles with𝐴𝐷 and𝐵𝐷, centered at 𝐹 and𝐺 respectively.𝐴𝐷 intersects⊙(𝐵𝐷𝐸) again at𝐼 and𝐵𝐷 intersects⊙(𝐴𝐷𝐸) again at 𝐻

    Figure S5 ( shortlisted): Let△𝐴𝐵𝐶 be an acute-angled triangle and 𝐷 be its incenter. The projection of𝐷 on𝐴𝐵, denoted as𝐸, forms two circumcircles with𝐴𝐷 and𝐵𝐷, centered at 𝐹 and𝐺 respectively.𝐴𝐷 intersects⊙(𝐵𝐷𝐸) again at𝐼 and𝐵𝐷 intersects⊙(𝐴𝐷𝐸) again at 𝐻. Denote the antipode...

  125. [133]

    Circle𝐸 and𝐷 pass𝐴

    Figure S6 ( shortlisted): Let△𝐴𝐵𝐶 be a scalene triangle, 𝐴𝐵𝐶𝐷 and 𝐴𝐶𝐵𝐸 are two paral- lelograms. Circle𝐸 and𝐷 pass𝐴. An arbitrary line through𝐴 meets the two circles again at S7 𝑄 and𝑃. Let𝑄′ and𝑃′ denote the reflections of 𝑄 against𝐵 and𝑃 against𝐶, respectively. 𝐹 being the i...

  126. [134]

    𝐸 is on line 𝐴𝐵 and𝐶𝐷⊥𝐶𝐸

    Figure S7: Let △𝐴𝐵𝐶 be an acute-angled triangle and 𝐷 be 𝐴𝐵’s midpoint. 𝐸 is on line 𝐴𝐵 and𝐶𝐷⊥𝐶𝐸 . The line linking the midpoint 𝐻 of minor arc 𝐴𝐸 in⊙(𝐴𝐶𝐸) and the midpoint𝐼 of minor arc𝐵𝐸 in⊙(𝐵𝐶𝐸) intersects⊙(𝐴𝐶𝐸) again at𝐽 and⊙(𝐵𝐶𝐸) again at 𝐾.𝐽𝐸 meets⊙(𝐵𝐶𝐸) again at 𝐿 and𝐾𝐸...

    2024

  127. [135]

    𝐻 is the circumcenter of ⊙(𝐷𝐸𝐹)

    Figure S8: Let △𝐴𝐵𝐶 be an acute-angled triangle, 𝐷, 𝐸, 𝐹 be feet corresponding to 𝐴, 𝐵,𝐶, respectively.𝐺 is△𝐴𝐵𝐶’s orthocenter. 𝐻 is the circumcenter of ⊙(𝐷𝐸𝐹). 𝐼 is the circumcenter of⊙(𝐵𝐶𝐺). Prove𝐻 is the mid point of𝐴𝐼

  128. [136]

    𝐺 is△𝐴𝐵𝐶’s orthocenter

    Figure S9 ( selected): Let△𝐴𝐵𝐶 be an acute-angled triangle,𝐷,𝐸,𝐹 be feet corresponding to 𝐴, 𝐵, 𝐶, respectively. 𝐺 is△𝐴𝐵𝐶’s orthocenter. 𝐻 is a point on 𝐴𝐵 such that 𝐷𝐻 is parallel to𝐴𝐶.𝐼 is the circumcenter of⊙(𝐴𝐷𝐻).𝐽 is another intersection of 𝐴𝐶 and⊙(𝐼). 𝐾 is the intersecti...

  129. [137]

    𝐸 is on 𝐴𝐶 such that ∠𝐸𝐵𝐶 is a right angle.𝐹 is the reflection of𝐸 over𝐵.𝐺 is the reflection of𝐹 over𝐶

    Figure S10: Let △𝐴𝐵𝐶 be an acute-angled triangle, 𝐷 be 𝐵’s foot. 𝐸 is on 𝐴𝐶 such that ∠𝐸𝐵𝐶 is a right angle.𝐹 is the reflection of𝐸 over𝐵.𝐺 is the reflection of𝐹 over𝐶. Denote the intersection of 𝐵𝐺 and 𝐴𝐶 as𝐼 and the mid point of 𝐵𝐼 as𝐽.𝐻 is the circumcenter of ⊙(𝐵𝐷𝐹). Prove𝐻...

  130. [138]

    Figure S11: Let △𝐴𝐵𝐶 be an acute-angled triangle and 𝐷 the intersection of 𝐴𝐵 and ∠𝐶’s internal angle bisector.𝐸 is the projection of𝐴 on𝐵𝐶.𝐹 is the reflection of𝐴 over𝐸.𝐺 the reflection of 𝐹 over𝐶.𝐻 is the circumcenter of⊙(𝐴𝐶𝐺). 𝐼 is another intersection of 𝐶𝐷 with⊙(𝐻).𝐽 is t...

    2024

Pith tools

Reviewed August 11, 2026 · model on record in the stance chip above.