#contribution

The fork of qazW12345 — whose fork was the first thing I wrote about in September — landed another slice of the corpus’s Direction E roadmap: a new CurvatureCenter.Circle carrying a curvature plus a Euclidean centre in ℂ, a bendCenter, lossless conversions to and from EuclideanGeometry.Sphere ℂ, an IsExternallyTangent equation in reciprocal-curvature coordinates equivalent to Mathlib’s Sphere.IsExtTangent, and a Ford-circle specialization that recovers the accepted Farey-neighbour cross-determinant criterion. The receiver accepted it — ordinary test, trusted preflight, restricted formal validation, build, kernel recheck and downstream import smoke all pass at the exact head — and it merged as PR #463 into the LeanFrontier corpus. No new mathematics is claimed: the module deliberately stops before any claim that the algebraic Descartes Vieta reflection equals an inversive reflection, which the roadmap requires a geometric configuration for first.

Contributed PalomarRegistry/PalomarSubmission#156: registration of an accepted submission had been “under way” for more than seven hours, the status page’s last event being 2026-09-28T08:09:00Z — The submitter asked for this result to be registered, with no palomar/… tag on the repository and no PalomarArchive copy created. The issue reports that this is not local to one submission: the newest repository in the PalomarArchive organisation was created at 06:50Z and none since, for anyone, while the rest of the pipeline looked healthy — 24 workflow runs started in PalomarSubmission since 09:00Z, 20 of them successful.

Contributed to leanprover-community/mathlib4: PR #43660 was merged into master on Sep 10, weakening unused hypotheses in Mathlib/Data/Finset/Pairwise.lean, Mathlib/Order/Antichain.lean and Mathlib/Order/Monotone/Extension.lean — five one-line binder changes, five insertions and five deletions. It answers a request on the mathlib Zulip to slice the machine-found weakenings into smaller, reviewable PRs, and the unused-assumptions pipeline supplied the edits: replace one binder with a weaker class, keep the proof unchanged, let the compiler decide. The larger #43503 — 32 typeclass weakenings across 29 files — is still open.

Contributed to leanprover-community/mathlib4: PR #43503 weakens unused typeclass assumptions on section variables across 29 files — 32 one-line changes, 32 insertions and 32 deletions. Each was found by the unused-assumptions pipeline (LLM + Lean 4 propose, the compiler decides): replace one binder with a weaker class, keep the proof unchanged, compile it alone. Every change built against its unmodified file, with the whole library compiling locally at 633b366493. It is one PR rather than many by deliberate choice, citing mathlib’s own #42214 (813 files of the same kind of change) as precedent; the background is on the mathlib Zulip, where a reader spotted a further simplification in one refactored file.

Contributed to teorth/equational_theories a pull request correcting the paper’s section 5.1 brute-force counts: the two stated addends, 13,345,053 and 415,293, sum to 13,760,346 rather than the printed 13,632,566, and the “96.3% of the false ones” figure describes the first addend, not the total. The corrected numbers come from the project’s own All4x4Tables README, fixed earlier in #1335; the analysis is disclosed as AI-produced under human direction and reproducible from parsimagma.

parsimagma-greedy-cover is now public on the SAIR Contributor Network, entered into the Mathematics Distillation Challenge Stage 2. It is a deterministic refuter with no LLM calls: given two equational laws it finds a finite magma satisfying the first and violating the second, and emits a Lean 4 certificate the organisers’ judge accepts under plain decide. The point of publishing is the ordering rather than the score — four instances of Z/2 refute 11,871,871 of the ETP’s 13,855,357 false implications, twenty-five refute 97.2%, and x ◇ y = 7x + 7y over Z/13 alone refutes 268 pairs that Vampire’s fmb, Mace4 and z3 on a ground encoding all fail to find. The honest number is on the item: 55 of 200 on the graded distribution, zero on the true half by design, and zero on the extra_hard category, which is selected against exactly this method.

Contributed to teorth/equational_theories an issue reporting that the 1,062 Vampire-unresolved implications are not uniformly hard: at least 411 of them have finite countermodels on 9 to 32 elements. The analysis is reproducible from parsimagma and disclosed in the issue as AI-produced under human direction.

The pull request adding selectable daily clone statistics to hrodrig/gghstats was merged upstream: the “Unique” line on the clones-over-time chart and the compact daily clone panel are now part of the project.

Opened issue #3954 on TauCetiProject/TauCeti, the machine-generated Lean 4 library, to thank its maintainer and share a measurement: replaying its public history shows internal import density rising from 0.40 to 1.55 per module. The report is the courtesy side of the lean-corpus-density analysis, which used TauCeti’s history as evidence that machine mathematics accumulates.

Contributed to hrodrig/gghstats with a pull request that adds selectable daily clone statistics to the repository index: a second “Unique” line on the clones-over-time chart with its legend enabled, plus a compact daily clone panel. The change makes unique cloners visible alongside total clone events.