{"id":"74224b3c-0584-4596-b4b0-8801c1fe0068","arxiv_id":"2411.11938","paper_version":1,"verdict":"CONDITIONAL","confidence":"MODERATE","novelty_score":5.0,"correctness_risk":"medium","formal_verification":"none","parameter_count":0,"one_line_summary":"A refactored, user-friendly version of AlphaGeometry's symbolic solver that adds length and angle reasoning and Pythagoras, and proves one previously unsolved IMO problem with human-supplied auxiliary constructions.","lead":"This paper presents Newclid, an open-source reimplementation and extension of AlphaGeometry's symbolic geometry solver, with a cleaner interface, new metric-geometry predicates, and support for the Pythagorean theorem. The authors report that their solver, DDARN, can now prove one of the five IMO problems that AlphaGeometry could not, though human-supplied auxiliary points were used.","discovery_kind":"extension","skeptic_critique":{"model":"deepseek-v4-flash","headline":"DDARN's claim to solve IMO 2008 P1B may be seed-dependent: the proof relies on numerically-checked orientation predicates, while the two intersection points on each side are unordered in the problem statement.","rationale":"The reader's weakest assumption — that the numerical checks feeding the matching cache and the new predicates faithfully represent symbolic geometry semantics — is precisely the load-bearing point. The paper's own Section 5 supplies a documented example (IMO 2009 P2) where a DDAR proof's correctness depended on a random choice of intersection point, and the same class of risk applies to IMO 2008 P1B, where the ordering of the two intersection points on each side is not specified but can affect `same clock` and `nsameside`. If the numerical check accepts a false orientation or side relation, the proof in Appendix B could be an artifact of the seed, not a theorem. The human-added auxiliary points and rules added after studying the problem also weaken the benchmark claim, but that is a transparency issue; the numerical-soundness issue threatens the mathematical validity of the claimed solution. A single computational experiment — swapping the labels of the unordered intersection points — would reveal whether the proof is robust. If it is not, the headline result should be downgraded; if it is, the conditional verdict can be confirmed. I therefore align with the reader's CONDITIONAL verdict and recommend the concrete swap test as the decisive check.","tokens_in":46712,"tokens_out":3992,"duration_ms":42801,"concrete_test":"Run DDARN on IMO 2008 P1B with the definitions of A1 and A2 interchanged in the input file (and analogously for B1/B2 and C1/C2), using the same rule set and auxiliary points. The problem statement is invariant under this swap, so a sound solver should still prove `cyclic A1 A2 B1 B2 C1 C2`. If the proof fails, terminates without a solution, or produces a different orientation-dependent trace, the original proof is seed/label-dependent and is not a valid proof of the problem as stated. Additionally, replay the Appendix B proof steps with exact symbolic algebra to confirm that every same-clock-dependent inference holds without relying on the random diagram.","verdict_should_be":"CONDITIONAL","load_bearing_attack":"The central benchmark claim is that DDARN solves an additional AG-30 problem (IMO 2008 P1B). The proof in Appendix B extensively uses similarity/congruence rules (e.g., 'SAS 33', 'Similar Triangles 35', r34/r35/r58–r69) whose hypotheses include the predicates `same clock` and `nsameside`. Section 3.4.1 states these predicates are 'simply a numerical check, not verifiable symbolically'. Section 4.4.3 further explains that the matching cache pre-filters statements by numerically checking them against a random coordinate diagram. Section 5 explicitly documents that random coordinate assignment can flip triangle orientation and that DDAR's proofs are non-deterministic and can even be incorrect for a different random choice (IMO 2009 P2). In IMO 2008 P1B, points A1/A2 (and B1/B2, C1/C2) are the two intersections of a circle with a sideline; the problem statement does not specify which is which. The numerical diagram assigns coordinates and therefore fixes an ordering, and the orientation-dependent proof steps may rely on that specific ordering. If the proof is only valid for one random realization of the labeling while the theorem must hold for both, then the generated proof is not a sound proof of the stated problem. No evidence is given that the numerical checks are invariant under the symmetries of the problem, so the central 'solves an additional problem' claim is not established as a mathematical result.","agreement_with_reader":"agree"},"referee_report":{"model":"deepseek-v4-flash","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.","tokens_in":46900,"tokens_out":8545,"duration_ms":89027,"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":[{"comment":"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.","section":"Abstract, Section 1, Section 6.1, Appendix B"},{"comment":"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.'","section":"Section 3.4.1, Section 4.4.3, Section 5, Appendix B"},{"comment":"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.","section":"Section 3.4.3, Section 4.4.1"}],"minor_comments":[{"comment":"The word 'hypotetical' should be 'hypothetical' in the description of the environment layout.","section":"Section 3.2"},{"comment":"The typo 'AlghaGeometry' should be 'AlphaGeometry'.","section":"Section 4.4.2"},{"comment":"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.'","section":"Sections 6.2 and 6.5"},{"comment":"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.","section":"Appendix A and Appendix B"},{"comment":"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.","section":"Section 6.1"}],"recommendation":"major_revision","confidential_remarks":"The paper is transparent about the human-supplied auxiliary points and the target-specific rule r50, which is to its credit, but the abstract and introduction do not carry that qualification. The more serious issue is the uncertified reliance on numerically checked orientation predicates in the generated IMO 2008 P1B proof; given that Section 5 itself documents an incorrect proof from a different random choice in another IMO problem, the authors need to supply a soundness argument or an independent proof check before the benchmark claim can be accepted. This is fixable within the manuscript's scope by rewording the claim and adding evidence."},"author_rebuttal":null,"desk_editor":{"model":"deepseek-v4-flash","letter":"Newclid is a genuine, usable piece of software and the paper is worth reading for anyone building on AlphaGeometry. But the headline result—that DDARN solves an additional AG-30 problem—comes with two material qualifications that are easy to miss from the abstract: the auxiliary points are human-supplied, and two of the rules used in the proof (r49, r50) were added after studying the problem. On top of that, the proof relies on numerically-checked orientation predicates, and the paper itself documents that these can flip with the random diagram. So the 'solves an additional problem' claim is not yet established as a stable mathematical result.\n\nWhat is actually new and good: the code is open-source, modularized, installable via PyPI, and independent of the Meliad library. The new predicates (lconst, aconst, rconst, same clock, nsameside) and the Pythagoras support genuinely widen the solver's scope. The CLI, GeoGebra input, and the visualization of dependency and symbol graphs are real improvements for debugging and for education. The paper is unusually honest about its limitations: it states that r50 was detected by studying the target problem, it explains the nondeterminism in DDAR, and it even shows an IMO 2009 P2 proof that becomes incorrect under a different random choice. That candor is creditworthy.\n\nThe soft spots are real but proportionate. The benchmark claim is overstated in the abstract: 'DDARN solves an additional problem' should carry the caveats of human auxiliary points and problem-tuned rules. More importantly, the stress-test concern about seed dependence is plausible and not addressed. The proof in Appendix B uses orientation-dependent similarity and congruence rules whose hypotheses include same clock and nsameside, both of which are numerical checks. The problem statement leaves A1/A2 (and the other pairs) unordered, but the numerical diagram fixes an ordering. Since the paper proves that random coordinates can flip triangle orientation and that this can change the correctness of a proof, the P1B proof might only be valid for one random labeling of the points. No invariance argument is given. That means the central claim is not a sound mathematical result as presented, though the software itself remains useful.\n\nA serious referee should engage with this paper. The software contribution deserves peer review, but the authors should be asked to correct the abstract, document or justify the soundness of the numerical predicates, and either show the P1B proof is independent of the random seed or downgrade the claim to 'solves with a specific seed and human-supplied auxiliary points.' I would cite this paper if I were working on geometry solvers, and I'd bring it to a reading group interested in automated theorem proving.","headline":"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.","tokens_in":47497,"tokens_out":2983,"would_cite":true,"duration_ms":28105,"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":"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…","keywords":["geometry theorem proving","symbolic solver","AlphaGeometry","DDAR","metric geometry","Pythagorean theorem","automated reasoning","IMO 2008 P1"],"falsifier":"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.","tokens_in":46460,"feed_emoji":"📐","tokens_out":4567,"duration_ms":42347,"temperature":0.7,"pith_summary":"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.","feed_headline":"Refactored geometry solver cracks an IMO problem AlphaGeometry missed","feed_subtitle":"DDARN adds metric predicates, Pythagoras, and explicit proofs, solving IMO 2008 P1B.","key_machinery":"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.","core_discovery":"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.","pith_inferences":["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."],"forward_implications":["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."],"supporting_citations":[{"why":"Defines AlphaGeometry, the DDAR solver, the AG-30 dataset, and the five unsolved problems that Newclid targets; supplies the baseline showing DDAR cannot solve IMO 2008 P1B.","marker":"[Trinh et al., 2024]"},{"why":"Introduces the deductive-database geometry engine and predicate formalism on which DDAR and DDARN are built.","marker":"[Chou et al., 2000]"},{"why":"Provides the JGEX formal language whose predicates and definitions AlphaGeometry and Newclid inherit for problem input.","marker":"[Ye et al., 2011]"}],"fun_headline_variants":["New geometry solver cracks IMO problem that stumped AlphaGeometry","DDARN upgrades AlphaGeometry, solves one more IMO geometry problem","Newclid's DDARN proves a new theorem AlphaGeometry couldn't","Refactored solver nails an IMO problem with new circle rules","From AlphaGeometry to Newclid: A solver that goes further"],"cache_read_input_tokens":3200,"weakest_assumption_plain":"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.","fun_headline_variants_meta":{"raw":{"variants":["New geometry solver cracks IMO problem that stumped AlphaGeometry","DDARN upgrades AlphaGeometry, solves one more IMO geometry problem","Newclid's DDARN proves a new theorem AlphaGeometry couldn't","Refactored solver nails an IMO problem with new circle rules","From AlphaGeometry to Newclid: A solver that goes further"]},"model":"deepseek-v4-flash","effort":"low","cost_usd":0.000698,"raw_usage":{"total_tokens":3169,"prompt_tokens":975,"completion_tokens":2194,"prompt_tokens_details":{"cached_tokens":384},"prompt_cache_hit_tokens":384,"prompt_cache_miss_tokens":591,"completion_tokens_details":{"reasoning_tokens":2103}},"tokens_in":591,"tokens_out":2194,"duration_ms":14042,"temperature":1.0,"reasoning_tokens":2103,"cache_read_input_tokens":384,"cache_creation_input_tokens":0},"cache_creation_input_tokens":0},"created_at":"2026-08-12T18:13:40.567477+00:00","model_set":{"reader":"deepseek-v4-flash"},"falsifier":"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.","supporting_citations":[{"cited_title":"A deductive database approach to automated geometry theorem proving and discovering","cited_arxiv_id":null,"evidence_quote":"Introduces the deductive-database geometry engine and predicate formalism on which DDAR and DDARN are built."}],"review_version":1}