CONCLUSIONS.md

Conclusions, evidence, and scope

This document turns “what did Litex actually achieve in IMO geometry?” into checkable claims. Each claim names its evidence and its counterexample/limit.

Claim A: Litex can define the geometry vocabulary IMO problems need

Claim. Points, vectors, dot product, determinant, squared distance, lines, circles, segments, rays, collinearity, perpendicularity, parallelism, midpoints, angles, congruence, similarity, concyclicity and related predicates can all be defined directly in Litex, without an external geometry library or a geometry-specific DSL.

Evidence.

• Archived shared library: IMO/Litex/geo/library_final.lit, 200 lines, 7,306 bytes, 39 declarations.
• The first 10 are function/set definitions; the remaining 29 are predicates, including is_on_segment, is_collinear, is_perpendicular, is_parallel, is_midpoint, is_angle_bisector, are_triangles_congruent, are_triangles_similar, are_concyclic, etc.
• New-format code: code/2D_Geometry/geo_definitions.lit is the same vocabulary in Litex 1.x syntax; geo.lit adds 186 verified theorems for 227 declarations total.
• Each new-format problem package also embeds the definitions it needs. For example, code/2D_Geometry/IMO/problem_12/solution.lit defines vec, det, is_triangle and is_strictly_inside_segment at the top and imports nothing.

Limit. This is not “zero library.” The archive used a 7.3 KB shared library; the new code distributes definitions into each package. Both show that the library is small and self-built, not that a full IMO proof was written from an empty file.

Who built the vocabulary. The adjacent automated definition experiment reports 39/39 definition tasks passed with zero axiom debt, and the archived IMO geometry library is the same scale (39 declarations). This shows the vocabulary is small and machine-buildable; the archived file is curated, not byte-identical to the pipeline output.

Terminology. “Without a library” in this document means “without a pre-existing Lean/Mathlib-scale external geometry library.” The agent still built and used a small internal Litex library; the new-format code embeds definitions per package. This is not “an empty file.”

Claim B: the archived experiment verified 11 IMO geometry problems

Claim. With Litex 0.9.116-beta and the 39-declaration library above, 11 of 12 problems and 14 of 15 packages passed strict verification; the strict traces contain no trust.

Evidence.

• Per-problem table: results/imo_runs.md, results/imo_runs.csv.
• Machine index: evidence/archived_verification_status.json, generated by tools/summarize_archived_runs.py from the original litex_verified.json / litex_strict.json files.
• Representative strict reports:
  • 1967 P1: 92 strict documents, all successful, 0 trust, both the necessity and sufficiency directions appear in the trace.
  • 1969 P4: litex_strict.json success, 0 trust.
  • 1970 P1: litex_strict_verified.json success, 0 trust.
• The single trust mention in an ordinary trace is the ordinary-mode warning that imported modules were not verified. Strict mode has 0. Do not use the ordinary warning to deny the strict result.

Counterexample. 1970 P6 (100 points, at most 70% acute triangles) did not converge in the archived run; production_problem20_strict.json is an error. The correct archived claim is 11/12, not 12/12.

Claim C: this is not just coordinate arithmetic

Claim. The verified set covers coordinate computation, trigonometric identities, area/ratio inequalities, constructive iff statements, concyclicity/tangency, covering problems and combinatorial geometry.

Evidence (problem → theme).

• Coordinates/trigonometry: 1960 P3, 1961 P5, 1962 P6, 1968 P1.
• Area/inequality: 1961 P4, 1966 P6.
• Construction/iff: 1961 P5, 1967 P1.
• Circles/tangency/concyclicity: 1962 P6, 1969 P4, 1970 P1.
• Polygons/vectors: 1963 P3.
• Combinatorial geometry: 1970 P6 (failed in the archive; later proof exists in the new code).

This shows that the Litex encoding can carry definitions, lemmas, constructions, contradiction and case analysis — not only “substitute coordinates and simplify.”

Claim D: the Lean/Mathlib gap is an engineering loop, not kernel incapability

Claim. Mainstream Lean work is strongest in algebra, number theory and combinatorics; plane geometry lacks a lightweight, unified, directly reusable IMO-level pipeline. Mainstream work therefore either skips geometry or builds a separate geometry DSL.

Evidence/support.

• AlphaGeometry uses a custom geometry language plus a deduction engine rather than handing geometry problems directly to Lean.
• Work such as LeanEuclid builds a dedicated Lean benchmark/library for Euclidean geometry; that need itself shows the missing ready-made pipeline.
• Lean/Mathlib has Euclidean/affine space foundations, but not a 7 KB-level unified interface for the point-line-circle-angle-similarity-concyclicity vocabulary used by IMO geometry.

Limit. This is an engineering judgment, not a mathematical-capability judgment. Lean can formalize geometry with more library work. This directory does not run a “Lean completely fails” control experiment. The defensible strong claim is:

In the dimension of “lightweight, unified, reproducible IMO geometry loops,” Litex has a working loop; the Lean/Mathlib ecosystem currently has no equally lightweight ready-made loop.

Claim E: the new-format code is the readable/reproducible version, with a version caveat

Claim. code/2D_Geometry/ is a complete copy of the upstream 1.1.1-beta tag. It uses Litex 1.x syntax (p(1), have points set, self-contained packages). It is the version to read; legacy 0.9.x code should not be run directly on 1.1.x.

Evidence.

• Upstream README states that 15 packages pass strict verification with Litex 1.0.6-beta, checked 2026-10-11.
• code/STATUS.md records our measured results with 1.0.6-beta and 1.1.1-beta; do not confuse the upstream claim with a local measurement.
• Legacy code uses p[1] indexing; new code uses p(1) function application and embeds definitions in each problem directory.

Limit. Litex 1.1.x proof search/normalization differs from 1.0.6. Some new-format packages fail on 1.1.1 because the engine no longer performs the same automatic reassociation of products; this is a version-compatibility issue, not a mathematical error. In addition, IMO/problem_17 did not finish within 1 h 42 min on 1.0.6 in our test and was stopped; the archived 0.9.116 P17 report passed, but the new P17 package is not practically reproducible end-to-end here. For a full reproducible run today, use tools/build_litex.sh 1.0.6-beta, or follow code/STATUS.md.

Claim F: the cost is high and token data is missing

Claim. The archived 11 solved problems took about 48 hours of wall-clock time across 14 packages; including the unfinished P20, about 59 hours. Individual packages range from 26 minutes to 14 hours. The archived logs do not record API token usage.

Evidence.

• results/imo_runs.csv, columns wall_clock and wall_clock_source.
• Time sources are of three kinds: metadata start/finish, first/last log timestamps, and agent-reported time. Each row names its source.
• Tokens: the archived logs contain no numeric prompt_tokens, completion_tokens or total_tokens. results/token_availability.md documents this and gives the adjacent geometry-library construction numbers only as an order-of-magnitude reference.

Limit. Wall-clock time includes model latency, rate limits, retries and human intervention; it is not pure proof-search time and is not directly comparable to Lean compile time.

Claim G: what the results do and do not support

Supported.

• Litex can define IMO geometry concepts from coordinates/sets in one language.
• Those definitions carry 11 IMO geometry problems through strict verification with zero trust.
• The loop does not depend on a Lean/Mathlib-scale external geometry library; the archived library is 7.3 KB and the new code is self-contained per problem.
• Relative to the Lean/Mathlib geometry engineering gap, this is a substantive contribution.

Not supported.

• “Litex is fully autonomous and unsupervised on IMO geometry.” The logs show repeated human corrections.
• “Zero library, zero seed.” The archive has a 39-declaration library; the new code has per-problem definitions.
• “12/12 passed.” Archived P20 did not complete.
• “Lean cannot do geometry at all.” Lean can; it lacks a lightweight unified ready-made pipeline.
• “Token cost is known.” The archived logs did not record it.

Claim H: a general LLM learned Litex and wrote checkable geometry

Claim. The archived proofs were produced by general-purpose LLMs (mostly gpt-5.6-sol, with some claude-opus-4-6 sessions), not by a geometry-specific prover and not by a model fine-tuned on Litex. The model learned Litex from a short guide and structured compiler feedback, wrote new definitions and helper lemmas, and repaired its own proof scripts until the strict kernel accepted them.

Evidence.

• The logs record the model name, the guide reads, the .lit writes, the compiler errors and the retries for each problem.
• The agent created problem-specific predicates and lemmas (for example is_strictly_inside_segment, is_cevian_ratio, is_subtended_tangent, determinant-factorization lemmas, ratio identities) rather than filling a fixed proof template.
• The logs show repeated error-driven repairs: explicit equality chains for algebraic substitutions, nonzero/positivity facts for well-definedness, disjunction/case encodings, and cross-file namespace fixes.
• The final reports are strict: no trust, no user axiom.

Limit. This is not “a weak model solved IMO geometry with no help.” The model is a capable general model, and humans imposed constraints and sometimes told it to continue. The claim is specifically about learnability of Litex and the kernel-checked output, not about unsupervised autonomy.

One-sentence summary

General-purpose LLMs learned Litex from a short guide and compiler feedback, then used a 7.3 KB self-built geometry library to strictly verify 11 IMO geometry problems (14 packages), covering coordinates, trigonometry, inequalities, constructions, circles/tangency and polygons. This establishes that a “learnable unified language + small library + strict kernel” geometry loop is feasible, and it fills the engineering layer where Lean/Mathlib is currently thinnest. But P20 did not complete, the cost is high, token usage was not recorded, and Lean is not incapable of geometry — those limits belong with the achievement.