[submission] morley_theorem — UNICO/NOUS pipeline (Claude by Anthropic)

[Solarys431]

Submission URL

https://github.com/Solarys431/unico-lean-proofs/tree/a5f503014a635623ec2d2de8ab0f6c00030d9028

Model

UNICO/NOUS pipeline — Claude (Anthropic)

How this solution was produced (optional)

Produced by an autonomous theorem-proving and certification pipeline built with Claude Code, directed and operated by a non-mathematician developer. All mathematics is AI-generated (Claude by Anthropic); exact polynomial cofactors for the linear_combination steps were computed symbolically with sympy and verified before kernel certification. The pipeline accepts nothing unless the local Lean kernel certifies it; this workspace was additionally verified locally with the official comparator at the CI-pinned tool commits (landrun 5ed4a3db, lean4export 3de59f10, comparator 71b52ec2) on the pinned toolchain (v4.32.0-rc1): "Your solution is okay!".

The proof is independent of all previously recorded solutions (none were consulted). It transports the benchmark's unoriented-angle configuration, via barycentric coordinates that recover the orientation sign from the convex-hull hypothesis, onto an oriented-ray complex-plane Morley development (Connes-style algebraic core closed by linear_combination with exact cofactors; ray-intersection master lemma; Complex.arg toolkit). A standalone statement with existence/uniqueness (∃!) and non-degeneracy companions lives in the same repository (UnicoProofs/Morley.lean). Axioms: propext, Classical.choice, Quot.sound only — no sorry, no native_decide.

Estimated cost: one afternoon of wall-clock time end-to-end (bridge design + proof + hardening, ~25 local kernel verdicts), subscription-based model usage, consumer Apple Silicon hardware. Human role: direction, operation and review of process — not of the mathematics. Context: announced on the Lean Zulip ("Morley's theorem (#84): AI-generated proof, please check", 2026-07-13, #AI authored projects), where Jeremy Chen kindly pointed us to this benchmark.

Acknowledgements

• I understand that the lean-eval CI will fetch my submission URL and run comparator on every lakefile.toml whose name matches a benchmark problem id.
• I understand that only the set of solved problem IDs, along with the metadata I entered above, will be published to the public leaderboard results store.
• I understand that an encrypted copy of the submission source tree (compressed gzipped tar, ≤ 10 MiB) is retained indefinitely in the private leanprover/lean-eval-audit repository for audit purposes, decryptable only by a small set of benchmark maintainers listed in .audit/recipients.txt. See docs/audit-archive.md.

[Solarys431]

Superseded by #780 (submitted via the issue form so the submission label is applied — this one was opened via API and never picked up the label, so no workflow could trigger). Apologies for the noise.