Pith. sign in

REVIEW 3 major objections 5 minor 7 references

Newclid: A User-Friendly Replacement for AlphaGeometry

T0 review · 3 major / 5 minor · reviewed 2026-08-12 · deepseek-v4-flash

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

Pith's one-line read This paper presents Newclid, a refactored symbolic geometry solver based on AlphaGeometry, and shows it solves IMO 2008 P1B, a problem the original system could not solve, by adding metric predicates, new rules, and human-guided auxiliary…

desk verdict Useful open-source refactor of AlphaGeometry's symbolic solver, but the headline solved-problem claim is weaker than the abstract suggests and likely seed-dependent. read the letter →

arxiv 2411.11938 v1 pith:PYZWMBSC submitted 2024-11-18 cs.GR cs.AI

Vladmir Sicca , Tianxiang Xia , Mathïs Fédérico , Philip John Gorinski , Simon Frieder , Shangling Jui This is my paper · ORCID
classification cs.GRcs.AI
keywords geometrytheoremprovingsymbolicsolverAlphaDDARmetricPythagoreanautomatedreasoningIMO2008P1
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

The paper claims that a careful, modular refactoring of AlphaGeometry's symbolic engine—not a bigger language model—can both make the system usable and extend what it can prove. The new solver DDARN adds predicates for lengths, constant angles, ratios, and orientation, plus rules including the Pythagorean theorem and two missing circle facts, and it makes every proof step traceable to explicit rules. Re-running the five AG-30 problems that AlphaGeometry could not solve, DDARN (with human-supplied auxiliary points O1, O2, O3, and O) solves one extra problem, IMO 2008 P1B, which requires showing six points are concyclic. A sympathetic reader should care because it demonstrates that the symbolic core was the bottleneck, and that transparency and extensibility can directly translate into problem-solving scope.

What carries the argument

The engine is a deductive database of rules applied breadth-first, backed by an algebraic reasoning (AR) module that tracks linear equations among angles and log-ratios. The load-bearing new objects are the Predicate classes, especially the numerically checked predicates same clock, nsameside, and PythagorasConclusions, which feed a matching cache built by checking all candidate statements numerically at the start of a problem. Centralized predicate classes let a user or agent add new theorems by writing one line in the rules file; the paper's new rules r49–r51 and the Pythagoras rule r57 are the concrete instances that expand the provable scope.

What would settle it

Run DDARN on a problem where two points have the same numeric orientation under random coordinate assignment but are symbolically distinct, and check whether same clock lets the engine derive a similarity or congruence that is false; or run IMO 2008 P1B with rules r49 and r50 removed from the rules file to confirm the proof fails, isolating whether the new rules are genuinely load-bearing.

Watch

Extended reading notes

Core claim

The central discovery is that DDARN, with its expanded predicate set and explicit orientation checks, solves IMO 2008 P1B in breadth-first-search mode, while the original DDAR cannot—even when given the same extra points. The key additions are rules r49 and r50 (points on a circle are equidistant from its center, and the intersection of perpendicular bisectors of non-parallel chords is the center), which were found by probing DDAR with small circle problems and were needed to complete the proof. The paper also shows the proof relies on the new same clock and nsameside predicates to make triangle similarity and congruence orientation-explicit, and on the lconst, aconst, rconst, and the compute predicates to handle metric statements and the Pythagorean theorem.

Load-bearing premise

The soundness of every proof depends on the numerical pre-checks that feed the matching cache and the new numerically-checked predicates (same clock, nsameside, PythagorasConclusions) correctly capturing the intended symbolic meaning of orientation, same-side, and right-triangle facts—if any of these numeric tests accepts a relation that is actually false in the geometry, a printed proof can be invalid even though every step cites a rule.

Editorial extensions

If this is right

  • DDARN expands the solvable problem class to metric geometry: lengths, fixed angles, ratios, and Pythagorean reasoning are now expressible and provable.
  • Proofs become auditable: every dependency, including previously hidden orientation checks and intrinsic rules, is recorded in a dependency graph and shown in the proof trace.
  • The solver is now steerable by agents (human, BFS, dummy, and future LLM), allowing auxiliary points to be added interactively and proof search to be guided.
  • With the seed mechanism, randomized coordinate assignment no longer silently changes proofs; reproducibility is restored.
  • If the pattern generalizes, other symbolic provers can adopt the predicate-class refactor and numeric pre-check cache to widen their scope without a larger neural model.

Reading between the lines

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

  • The paper's evidence suggests the limiting factor in AlphaGeometry was the symbolic engine's vocabulary, not the LLM—implying that complementary upgrades to DDAR-style engines may yield further IMO problems without scaling the model.
  • The same numerical-check-to-symbolic-cache technique could be extended to other numerically inspired predicates, such as incircle-versus-excircle distinctions or point-in-triangle relations, as long as the numeric checks are made explicit predicates.
  • A direct testable extension would be to run DDARN on the full AG-231 dataset to see whether the new rules and metric predicates increase the solve rate beyond the reported IMO-30 gains.
  • One could also integrate the new predicates with an LLM to see whether the expanded rule set reduces the number of auxiliary points the model must propose.
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 / 5 minor

Summary. The paper presents Newclid, an open-source refactoring of AlphaGeometry centered on the DDARN symbolic solver. The claimed contributions are: a user-facing CLI and GeoGebra input, an agent interface for steering the solver, modular code with visualization and debugging tools, new predicates for angles, ratios, lengths, and orientation, a Pythagorean-theorem rule, and improved reproducibility via seeds. The headline evaluation claim is that DDARN 'solves an additional problem' from the AG-30 benchmark, namely IMO 2008 P1B, which AlphaGeometry could not solve. The solution is obtained with four human-supplied auxiliary points and after adding rules r49 and r50.

Significance. If the claims were fully established, the paper would be a useful engineering contribution: the code is open-sourced, the refactoring separates the solver from the LLM dependencies, the visualization of dependency and symbol graphs is genuinely helpful for debugging, and the explicit treatment of previously hidden orientation checks is a step toward transparency. The honest discussion of nondeterminism in Section 5 is also valuable. However, the central benchmark claim is materially weaker than the abstract suggests: the additional problem is solved only after human construction of four auxiliary points and after rule additions that were partly tuned on the very same problem. In addition, the generated proof relies on numerically checked orientation predicates whose soundness and label-invariance are not established. As a mathematical benchmark result, the paper needs qualification and supporting evidence; as a software/usability contribution, the claims are more solid.

major comments (3)
  1. [Abstract, Section 1, Section 6.1, Appendix B] The claim that 'DDARN solves an additional problem' from AG-30 is overstated as stated. Section 6.1 explains that the solution of IMO 2008 P1B required a human to prescribe four auxiliary points O1, O2, O3, and O, and Appendix B states explicitly that 'the auxiliary constructions were added by a human.' Moreover, Section 6.1 says that the need for rule r50 'was detected by studying this very problem,' so the rule set was partly tuned to make this benchmark solvable. The abstract and introduction should therefore not present this as a like-for-like comparison with AlphaGeometry's autonomous performance; the result should be labeled as 'DDARN with human auxiliary points and target-specific rule additions.' A table reporting whether the problem is solved by the original rule set, with the new r49/r50 rules, and with or without each auxiliary point would make the claim precise.
  2. [Section 3.4.1, Section 4.4.3, Section 5, Appendix B] The mathematical validity of the IMO 2008 P1B proof is not established. The proof in Appendix B uses similarity and congruence rules whose hypotheses include the predicates `same clock` and `nsameside` (rules r34, r35, r58-r69, and the steps labeled 'SAS' and 'Similar Triangles'). Section 3.4.1 states that these predicates are 'simply a numerical check, not verifiable symbolically,' and Section 4.4.3 explains that the matching cache pre-filters statements by numerical checks against a random coordinate diagram. Section 5 then concedes that random coordinate assignment can flip triangle orientation and that a DDAR proof for IMO 2009 P2 can be incorrect under a different random choice. In the formal translation of Section 6.1, the points a1/a2, b1/b2, and c1/c2 are defined as the two intersections without any ordering, so the numerical diagram fixes an arbitrary labeling. The paper gives no argument that the Appendix B proof is valid for all admissible labelings or for all random coordinate choices, and it does not report the seed used. To support the claim, the authors should either prove the invariance/symmetry of the proof under the relevant label swaps and random choices, or independently verify the generated proof with a checker that treats the numerical premises under an explicit and sound semantics, or weaken the claim to 'a proof was found for one numerical realization.'
  3. [Section 3.4.3, Section 4.4.1] The treatment of the Pythagorean theorem raises a soundness question for the expanded-scope claim. The paper says that the `PythagorasConclusions` predicate 'has a method to extract the distance of the missing side of the triangle (if there are two known sides) numerically and add the corresponding lconst statement to the proof state, avoiding the need for manipulating an equation.' This means the conclusion of the Pythagorean rule can be inserted purely on the basis of a numerical computation rather than a symbolic derivation. Unless exactness is guaranteed by the computation, any proof using this path is not a formal derivation of the stated theorem. The paper should clarify whether any of the proofs presented in the paper rely on this numerical extraction, and if so, how the exactness of the extracted lconst statement is certified.
minor comments (5)
  1. [Section 3.2] The word 'hypotetical' should be 'hypothetical' in the description of the environment layout.
  2. [Section 4.4.2] The typo 'AlghaGeometry' should be 'AlphaGeometry'.
  3. [Sections 6.2 and 6.5] The word 'undecidability' is used to mean that the current solver cannot express or prove the problem; this is not undecidability in the logical sense and should be rephrased as 'not solvable by the current deductive system' or 'outside the expressive scope of the formalism.'
  4. [Appendix A and Appendix B] The rule list in Appendix A says the active rules include r34 and r3, while Appendix B cites steps such as 'SAS 33', 'Similar Triangles 35', and 'Similar Triangles 39' that do not appear in the commented rule list with those names; the correspondence between the rule numbers and the names used in the proof trace should be made explicit.
  5. [Section 6.1] The phrase 'DDAR was not able to solve this problem even if provided the extra points' is helpful, but it would be even clearer to state which version of the rule set was used in that failed attempt, because the paper later reports that r49 and r50 were needed.

Circularity Check

1 steps flagged · score 6.0 of 10

The new benchmark success is partly tuned to the target: rule r50 was added specifically after studying IMO 2008 P1B, and the proof of that problem invokes r50 as a load-bearing step.

  1. fitted input called prediction [Section 6.1 (Discussion of IMO 2008 P1B); Appendix B, proof step 204]
    "Reviewing our proof, on the other hand, reveals the use of rules r49 and r50 (the need for rule r50, in fact, was detected by studying this very problem); see Appendix A."

    The central benchmark claim is that DDARN solves an additional AG-30 problem, IMO 2008 P1B, which AlphaGeometry could not solve. The paper explicitly states that the need for rule r50 was detected by studying this very problem, and the supplied proof invokes r50 at a key step (step 204: cyclic C1,C2,A1,A2 with OC1=OC2 and OA1=OA2 yields OC1=OA1 by r50). The paper also reports that the original DDAR rule set exhausted the search on this formulation, so r50 is load-bearing rather than incidental. Thus the solver's success is partially produced by a rule selected by inspecting the target problem itself, making the benchmark a tuning instance rather than an independent test of the rule set.

full rationale

The only clear circularity is the target-informed addition of rule r50. The paper admits that the need for r50 was detected by studying IMO 2008 P1B, and the Appendix B proof uses that rule to finish the concyclicity argument, so the newly solved benchmark is partly a product of rule-set tuning rather than a fully independent evaluation. The auxiliary point O and the other added definitions are not circular: they supply premises, not the conclusion. The numerical predicates same clock and nsameside and the matching cache raise soundness concerns about random orientations, but they are not circular in the sense of deriving the goal from itself; they are correctness risks. There is no load-bearing self-citation chain, and the refactoring, CLI, and GeoGebra contributions are independent engineering content. Score 6 reflects that the central benchmark claim is substantially weakened by one deliberately target-tuned rule, while the majority of the system and proof work remains independent.

Assumptions & free parameters 0 free parameters · 3 assumptions · 0 invented entities

The central benchmark result depends on the rule set and numerical checks listed above. No numerical parameters are fitted, but the rule set was adjusted to the target problem, making the benchmark not fully out-of-sample.

assumptions (3)
  • domain assumption The rules in rules.txt encode valid Euclidean geometry theorems.
    The solver's proofs are built by applying these rules, but the paper does not machine-check the soundness of the rule set.
  • domain assumption Numerical coordinate checks (same clock, nsameside, matching cache) correctly instantiate symbolic orientation and side relations.
    Sections 3.4.1 and 4.4.3 state these are numerical checks, not symbolically verifiable, yet they are used as hypotheses in similarity and congruence rules.
  • domain assumption The Pythagorean rule's numeric extraction of the missing side length is sound for all problem instances.
    Section 4.4.1: PythagorasConclusions adds an lconst statement from the numerical diagram rather than deriving it from symbolic equations.

how reviews work

0 comments
Cite this review

Pith. "Pith review of Newclid: A User-Friendly Replacement for AlphaGeometry." pith.science (2026). https://pith.science/paper/PYZWMBSC

@misc{pith2026241111938,
  author       = {Pith},
  title        = {Pith review of: Newclid: A User-Friendly Replacement for AlphaGeometry},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/PYZWMBSC}},
  note         = {Machine review of arXiv:2411.11938}
}
read the original abstract

We introduce a new symbolic solver for geometry, called Newclid, which is based on AlphaGeometry. Newclid contains a symbolic solver called DDARN (derived from DDAR-Newclid), which is a significant refactoring and upgrade of AlphaGeometry's DDAR symbolic solver by being more user-friendly - both for the end user as well as for a programmer wishing to extend the codebase. For the programmer, improvements include a modularized codebase and new debugging and visualization tools. For the user, Newclid contains a new command line interface (CLI) that provides interfaces for agents to guide DDARN. DDARN is flexible with respect to its internal reasoning, which can be steered by agents. Further, we support input from GeoGebra to make Newclid accessible for educational contexts. Further, the scope of problems that Newclid can solve has been expanded to include the ability to have an improved understanding of metric geometry concepts (length, angle) and to use theorems such as the Pythagorean theorem in proofs. Bugs have been fixed, and reproducibility has been improved. Lastly, we re-evaluated the five remaining problems from the original AG-30 dataset that AlphaGeometry was not able to solve and contrasted them with the abilities of DDARN, running in breadth-first-search agentic mode (which corresponds to how DDARN runs by default), finding that DDARN solves an additional problem. We have open-sourced our code under: https://github.com/LMCRC/Newclid

Figures

Figures reproduced from arXiv: 2411.11938 by the authors.

Figure 1
Figure 1. Index page generated for a single problem, with the diagram of the proof, the symbols [PITH_FULL_IMAGE:figures/full_fig_p007_1.png] view at source ↗
Figure 2
Figure 2. An exemplary problem in GeoGebra that can be parsed by Newclid. [PITH_FULL_IMAGE:figures/full_fig_p009_2.png] view at source ↗
Figure 3
Figure 3. Overview of interactions between different components of Newclid. [PITH_FULL_IMAGE:figures/full_fig_p016_3.png] view at source ↗
Figures from the paper (9 more)
Figure 4
Figure 4. Figure 4: A depiction of the reduced dependency graph containing the proof of a simple problem [PITH_FULL_IMAGE:figures/full_fig_p017_4.png]
Figure 5
Figure 5. Figure 5: A depiction of what the symbols graph of a small problem that could be solved by [PITH_FULL_IMAGE:figures/full_fig_p017_5.png]
Figure 6
Figure 6. Figure 6: The width at every depth of the dependency graphs, with levels ordered from statements [PITH_FULL_IMAGE:figures/full_fig_p019_6.png]
Figure 7
Figure 7. Figure 7: The DDARN symbols graph of the same problem as in Figure [PITH_FULL_IMAGE:figures/full_fig_p020_7.png]
Figure 8
Figure 8. Figure 8: The profiling of the level of functions where the matching of predicates occurs in the [PITH_FULL_IMAGE:figures/full_fig_p023_8.png]
Figure 9
Figure 9. Figure 9: Diagram for the statement of Problem 1 of the IMO 2008 exam. [PITH_FULL_IMAGE:figures/full_fig_p027_9.png]
Figure 10
Figure 10. Figure 10: Diagram for the statement of Problem 6 of the IMO 2008 exam. [PITH_FULL_IMAGE:figures/full_fig_p030_10.png]
Figure 11
Figure 11. Figure 11: Diagram for the statement of Problem 6 of the IMO 2011 exam. [PITH_FULL_IMAGE:figures/full_fig_p033_11.png]
Figure 12
Figure 12. Figure 12: Diagram for the statement of Problem 3 of the IMO 2021 exam. [PITH_FULL_IMAGE:figures/full_fig_p034_12.png]

Discussion (0). Continue with ORCID to comment.

Reference graph

Works this paper leans on

7 extracted references · 5 canonical work pages

  1. [1]

    A deductive database approach to automated geometry theorem proving and discovering

    Shang-Ching Chou, Xiao-Shan Gao, and Jing-Zhong Zhang. A deductive database approach to automated geometry theorem proving and discovering. Journal of Automated Reasoning, 25 0 (3): 0 219--246, 2000

    work page 2000

  2. [2]

    Hypertree proof search for neural theorem proving

    Guillaume Lample, Timothee Lacroix, Marie-Anne Lachaux, Aurelien Rodriguez, Amaury Hayat, Thibaut Lavril, Gabriel Ebner, and Xavier Martinet. Hypertree proof search for neural theorem proving. Advances in neural information processing systems, 35: 0 26337--26349, 2022

    2022

  3. [3]

    Wu's M ethod can B oost S ymbolic AI to R ival S ilver M edalists and A lpha G eometry to O utperform G old M edalists at IMO G eometry

    Shiven Sinha, Ameya Prabhu, Ponnurangam Kumaraguru, Siddharth Bhat, and Matthias Bethge. Wu's M ethod can B oost S ymbolic AI to R ival S ilver M edalists and A lpha G eometry to O utperform G old M edalists at IMO G eometry. arXiv preprint arXiv:2404.06405, 2024

    arXiv 2024

  4. [4]

    52nd International Mathematical Olympiad Problem : Shortlist With Solutions

    Bart de Smit, Ilya Bogdanov, Johan Bosman, Andries Brouwer, Gabriele Della Torre, G\'eza K\'os, Hendrik Lenstra, Charles Leytem, Ronald van Luijk, Christian Reiher, Eckard Specht, Hans Sterk, and Lenny Taelman. 52nd International Mathematical Olympiad Problem : Shortlist With Solutions . Technical report, International Mathematical Olympiad (IMO), Amsterd...

    work page 2011

  5. [5]

    Trinh, Yuhuai Wu, Quoc V

    Trieu H. Trinh, Yuhuai Wu, Quoc V. Le, He He, and Thang Luong. Solving olympiad geometry without human demonstrations. Nature, 625 0 (7995): 0 476--482, January 2024. ISSN 0028-0836, 1476-4687. URL https://www.nature.com/articles/s41586-023-06747-5

    work page 2024

  6. [6]

    On the decision problem and the mechanization of theorem-proving in elementary geometry

    Wen-Tsün Wu. On the decision problem and the mechanization of theorem-proving in elementary geometry. Scientia Sinica, 21 0 (2): 0 159--172, 1978. URL http://utest.sciengine.com/publisher/Science China Press/journal/Scientia Sinica/21/2/10.1360/ya1978-21-2-159

    work page doi:10.1360/ya1978-21-2-159 1978

  7. [7]

    An I ntroduction to J ava G eometry E xpert

    Zheng Ye, Shang-Ching Chou, and Xiao-Shan Gao. An I ntroduction to J ava G eometry E xpert. In Automated Deduction in Geometry: 7th International Workshop, ADG 2008, Shanghai, China, September 22-24, 2008. Revised Papers 7, pages 189--195. Springer, 2011

    work page 2008

Pith tools

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