LEAN4 AUTO YOUTUBE LIVING

A collaborative Lean 4 formalization of Mazur's torsion theorem

Bibliography of formalization/mechanization related mathematical logic

A Lean 4 formalization of the ternary (weak) Goldbach theorem, with an explicit audited finite and computational trust boundary.

Best-practice starter repository for Palomar submissions

[ICLR 2026] Divide and Abstract: Autoformalization via Decomposition and Abstraction Learning

Lean 4/Mathlib formalization of identities from Andrzej Odrzywolek’s “All elementary functions from a single operator” (arXiv:2603.21852).

Lean 4 and Mathlib formalization of nonuniform Berry–Esseen bounds and Bentkus's multivariate Gaussian approximation over convex sets.

Graduate-level interactive explainer for quantitative Collatz descent

Formalizing Algebraic Theory of General Topology in Lean

A Lean 4 study of the defect: an invariant of a positive-definite quadratic form on a finite-rank lattice measuring the failure of its spectrum to factor over the primes. Math amateur + LLM-coauthor, so.. you know.

Lean 4 formalization and paper proving cofinite zero-hitting by high derivatives of a transcendental entire function

Lean 4 formalizations of results from my research on graphs, networks, and the modulus of families of objects.

Formal Resolution of the Two-Dimensional Jacobian Conjecture in Lean 4 via Graded Differential Operators.

Lean 4 formalization for quantitative Collatz endpoint transport

Lean 4 formalization of Gleason's theorem via Busch's effects formulation

A Machine-Verified Constructive Proof of Lemoine's Conjecture.

First-passage linear transport for stretched-logarithmic natural-density Collatz descent

Workshop de Lean, SemUni '26

Preprint proving in Z_sep that no set carries exactly three pairwise nonisomorphic dense linear orders without endpoints, with a Level IV Lean 4 formalization.