Lean 4 proofs of the irrationality of Li₂(r) at certain rational points r
-
Updated
Sep 29, 2026 - Lean
Lean 4 proofs of the irrationality of Li₂(r) at certain rational points r
Rocq 9.1 formalization of the irrationality of pi via the Leibniz window method - all statements over Set carriers, zero axioms, extractable witnesses | 构造性π:Set 载体·零公理·见证可提取
ConstructiveWorld: zero-axiom constructive mathematics library (Rocq/Coq) - main line of the paper 'Constructive Strong Irrationality of pi' (frozen artifact: DOI 10.5281/zenodo.23717747)
AI-assisted research on e + pi: full proof attempts, scoped negative results, exact certificates, and community tasks. No accepted solution is claimed.
JavaScript double precision library.
Formal Verification of the 7-Color Chromatic Number of the Plane via Toroidal Projection and the Irrationality of 2π.
Developers seem to be irrationally afraid of CSS, somehow. This repository shows them they do not need to be.
Hankel-determinant rational approximation experiments for irrationality search. Rust Ferguson pipeline, shared Lean 4 `lean-prove` library, and finite-index checkpoints.
To associate your repository with the irrationality topic, visit your repo's landing page and select "manage topics."