Miscellaneous classical and other mathematical results, formalised in Lean 4 on top of Mathlib.

This repository is the product of two very different kinds of work, and it is worth being precise about which is which.

George A. Constantinides's contribution — selection, specification, and a best-effort read of each result's advertised statements. Which results are worth formalising at all; which are missing from Mathlib or awkward to use there; what each theorem should say and in what generality; which hypotheses belong in the statement; whether a generated result is worth keeping or should be thrown away; and the design of the checks in What this repository guarantees. This is the editorial and mathematical judgement that determines what the library contains, and it is not automatable.

Each result's advertised statements are also read against its informal claim before the result is published. A result's advertised statements are the declarations its ## Informal statement makes claims about, and its ## Provenance names them. That is the whole of what the read covers. A result file holds a great deal more — the lemmas its proof is assembled from, the definitions those lemmas need, and for a larger result whole supporting modules of both — and all of it is proof, whatever keyword introduces it, and may be read by no one. An advertised statement stated through a definition of this library's own is read together with that definition, since it cannot be read without it; that is why the house rule prefers there to be none.

That read is genuine but explicitly best-effort: one person, no second reader, none of the systematic scrutiny a Mathlib review would apply, and no reading of the proof. It removes some bad statements. It is not a warrant, and it is not a substitute for the check described in Reviewing a result in thirty seconds.

That read is preceded by a blind read-back. The advertised statements are given — with any definition they are stated through, and nothing else — to an agent that has not seen the informal statement, the source, or the rest of the file, and which writes out what they literally assert; the author then compares that rendering against the informal claim. The point is that every other guard here is applied by someone who already knows what the statement was meant to say, and therefore tends to see it — a read-back is the one reading not exposed to that. It is machinery, not a reviewer: it produces evidence, and the judgement about what the divergence means stays with one person. Where a read-back surfaced something, the result's ## Provenance section says so.

Claude's contribution — formalisation and proof. Given a result to prove, the Lean statement and its proof term are generated by Claude. Both are verified by Lean's kernel and audited; no human reads the proof itself, and no machine read of it is part of the process. Where a result has had one regardless — an independent model review, say — its ## Provenance says so and says exactly what was inspected; that is not a review either. No claim is made that the proof strategies are novel, elegant, or idiomatic — only that they are correct.

The consequence worth internalising: a mistake here will not be a wrong proof, because the kernel does not admit those. It will be a statement that does not say what it appears to say, of the kind a best-effort read can miss. That is what the conventions below are designed to make cheap for you to catch.

Mathlib's bottleneck is reviewer attention, and an unreviewed contribution costs it rather than helps it. Results here are too small, too scattered, too far outside Mathlib's mission, or too long in machine-generated proof to justify spending that attention on them. Mathlib is the right home for material many people will build on; this is a place for the rest. Anything here that turns out to be broadly wanted should be proposed upstream, where it will get the human review this repository deliberately does not provide.

Several other homes now exist for formalisation that Mathlib will not review, and they differ from each other — and from this repository — in what stands behind a result:

• Tau Ceti — an integrated library written entirely by AI contributors, directed by human-written roadmaps and gated by adversarial AI review against a fixed public rubric. Built for scale and reuse.
• Lean Pool — an archive of independent, completed formalisation projects, human- or AI-written, admitted on deterministic linters plus an LLM review of fit and significance.
• merely-true — AI-generated Lean under deliberately permissive rules, merged automatically once it compiles, from identified accounts.

All three build on Mathlib, are permissively licensed, and aim at a volume this repository does not. If what you want is a large body of formal mathematics to build on, look there before here.

What distinguishes this repository is not its review — it has none — but who is answerable for the selection, and how exactly the gap is described. A named person chose each result, specified what it should say, read its advertised statements against its informal claim, and has written down precisely which of those steps is a guarantee and which is not (see Who did what and What this repository guarantees). That does not scale, which is the point: it is why the library is small and expected to stay small, and why "it compiled" has never been enough for a result to land.

The one thing this repository cannot check for itself is whether a statement says what it claims to. Where that can get a second, independent read, it should. Palomar registers individual results, replaying their proofs through two independent kernels and checking each formal statement against its informal claim. It is explicitly not peer review and not an endorsement, but it is another pair of eyes on exactly the risk that matters here. A result that carries a registration says so under ## Provenance.

Add to your lakefile.toml:

[[require]]
name = "MiscMath"
git = "https://github.com/geoconuk/lean-misc-math"
rev = "v0.3.0"

Then import MiscMath for everything, or import individual modules (import MiscMath.Analysis.KolmogorovArnold) to keep your build light.

Pin to a tag rather than to main: statements here may be strengthened, corrected or withdrawn, and you want a fixed target. v0.3.0 is current, and each tag records the Mathlib version it was built against. main tracks whatever Mathlib the repository currently builds against and will move under you.

API documentation: https://geoconuk.github.io/lean-misc-math/docs/ (rebuilt on every push).

If these results are useful in your work, please cite the repository. The selection and curation of results is the contribution being credited, and a citation is what makes that contribution visible.

CITATION.cff carries the machine-readable metadata; GitHub renders a "Cite this repository" button from it. In BibTeX:

@software{constantinides_leanmiscmath,
  author  = {Constantinides, George A.},
  title   = {{lean-misc-math}: miscellaneous mathematical results formalised in {Lean 4}},
  year    = {2026},
  version = {0.3.0},
  url     = {https://github.com/geoconuk/lean-misc-math},
  doi     = {10.5281/zenodo.22648192},
  license = {Apache-2.0},
  note    = {Result selection by the author; Lean statements and proofs machine-generated
             and machine-verified}
}

Please cite the version or tag you actually used — statements may be strengthened, corrected, or withdrawn between releases. If you built against main rather than a tag, cite the commit hash instead of the version number.

Every release is archived on Zenodo. The DOI above is the concept DOI, which always resolves to the newest version; each release also has its own version DOI, reachable from that page. Cite the version DOI if you need to pin what you actually built against, and the concept DOI if you mean the library as a whole.

Guaranteed, mechanically, on every commit:

Not guaranteed:

• That a statement means what its docstring says it means. This is the real risk, and it is unautomatable. A theorem can be correctly proved, non-vacuous, axiom-clean, and still not be the theorem you wanted — because it quantifies over the wrong thing, uses truncated Nat subtraction, relies on a junk-value convention (x / 0 = 0), or is stated in terms of a bespoke definition rather than Mathlib's. Advertised statements do get a best-effort read from the author, against a blind read-back of the Lean (see Who did what), which removes some of these — but that is one person's judgement on one rendering, it is not a review, and it carries no guarantee.

  A result may also have had an independent machine check of the same correspondence, recorded under its ## Provenance as a Palomar registration; a result whose ## Provenance records no registration has none. That is a second reading by something that did not write the statement, and it is worth more than nothing — but Palomar is explicit that it is not peer review, not an endorsement and not a human read of the proof, so it does not convert any of the above into a guarantee. Nothing obliges a result to carry one.

• That anything other than an advertised statement has been read by anyone. A result file exports lemmas and definitions besides the statements it advertises, and a larger result exports whole support modules of them. They are kernel-checked and axiom-audited like everything else here, and that is all that is claimed for them: any of them may be read by no one. Where a result's documentation cites such a declaration by name — to bound what was not formalised, say, or to show a hypothesis cannot be dropped — it is pointing you at a kernel-checked fact whose statement you must read for yourself.

• That a result is not already in Mathlib, in better generality, under a name you would find by searching.

• That naming, generality, or API shape follows Mathlib conventions. They are aimed at it, not held to it.

The repository is structured so that checking the unguaranteed part is cheap. See below.

The author's best-effort read has already happened by the time a result is published, but it is one pair of eyes on the advertised statements, and nothing else is guaranteed any. Do your own check — every result file has the same shape, and you can convince yourself of a statement without reading its proof:

1. ## Informal statement — the claim in English. Compare it against the advertised statements. This is the check that matters, and it is the one you have to do yourself.
2. ## Source — a citation, so you can check the informal statement is the real theorem.
3. ## Provenance — who selected the result, which declarations were read, and what was machine-generated.
4. ## Sanity checks — examples that (a) exhibit values satisfying the hypotheses, so you know the theorem is not vacuous, and (b) confirm the conclusion at concrete values by decide or norm_num, independently of the proof. If a statement has drifted from its intent, these are usually where it shows.

docs/TEMPLATE.lean is the skeleton, with the requirements spelled out inline.

MiscMath.lean                  root; imports every result
MiscMath/Audit.lean            runs the library-wide axiom audit at build time
MiscMath/Meta/AxiomAudit.lean  the #audit_axioms command
MiscMath/<Area>/<Result>.lean  one result (or one tight cluster) per file
scripts/                       the textual CI guards
docs/TEMPLATE.lean             skeleton for a new result

lake exe cache get && lake build

lake build runs the axiom audit as part of the build — there is no separate step to forget. The shell guards run in CI and can be run locally:

./scripts/check-imports.sh && ./scripts/check-conventions.sh && ./scripts/self-test-audit.sh

Mathlib is pinned by tag in lakefile.toml and by commit in lake-manifest.json; both are committed. The Update Dependencies workflow proposes bumps as pull requests and opens an issue when a bump breaks the build, so the repository fails loudly rather than bit-rotting silently.

See CONTRIBUTING.md. Reports that a statement is wrong, misleading, or weaker than it appears are the most valuable contribution you can make here, precisely because that is what the automated checks cannot catch.

Apache 2.0, matching Mathlib, so that anything worth upstreaming can be.