Formal proof of CLT in Lean 4/Mathlib — autonomous agent output, no human intervention, no sorry
-
Updated
Feb 23, 2026 - Shell
#
lean4
Lean is a functional programming language that makes it easy to write correct
and maintainable code. You can also use Lean as an interactive theorem prover.
Lean programming primarily involves defining types and functions. This allows
your focus to remain on the problem domain and manipulating its data, rather
than the details of programming.
Here are 18 public repositories matching this topic...
Language-agnostic MPFS cage validator specification
-
Updated
Apr 13, 2026 - Shell
Cross-compiling the Lean 4 runtime for Android (aarch64-linux-android) with the NDK
-
Updated
Aug 25, 2026 - Shell
A /goal engine for Claude Code where completion is EARNED, not announced: acceptance criteria are real shell commands, the Stop hook re-runs every one of them, and only exit 0 ends the session.
shell bash hooks ci verification developer-tools formal-verification dtd lean4 anthropic llm-agents agent-tools claude-code claude-code-plugin stop-hook
-
Updated
Aug 24, 2026 - Shell
Turn any coding agent (Claude Code, Codex, Cursor, Copilot, Gemini CLI...) into a disciplined research machine for attacking open problems in mathematics — proof contracts, portfolio search, adversarial audits, exact-arithmetic verification. Implements Shouqiao Wang's 6-Erdős-problems-in-5-days workflow.
-
Updated
Jul 23, 2026 - Shell
Independent kernel-level verification of a claimed resolution of Erdős problem 1002: seven layers including a from-source bootstrap and lean4checker replay, with all 7,948 theorems axiom-clean.
theorem-proving lean formal-verification number-theory continued-fractions mathlib lean4 formalized-mathematics erdos-problems proof-auditing
-
Updated
Aug 2, 2026 - Shell
Lean 4 theorem proving skill and workflow pack for AI coding agents
-
Updated
May 22, 2026 - Shell
The Role of Thoughts: a Dynamic Cognitive Mixture-of-Experts router for Claude Code. 9 expert lenses, 10 routing lanes, an R/s+ divergence gauge -- specified in 1770 machine-checked Lean 4 theorems across 99 modules, with 797 mutants applied and 797 killed, and 84 checkers behind 83 release gates.
bash hooks router powershell theorem-proving agpl moe formal-verification eupl ai-agents proof-engineering mathlib mixture-of-experts lean4 prompt-engineering agentic-workflow claude-code claude-code-plugin llm-tooling machine-checked
-
Updated
Aug 30, 2026 - Shell
examples from https://adam.math.hhu.de/#/g/leanprover-community/NNG4
-
Updated
Mar 10, 2026 - Shell
Offline-ready Lean 4 + Mathlib Linux x86_64 bundle
-
Updated
Jun 12, 2026 - Shell
Descriptive Lean 4 formalization of the Open Knowledge Format (OKF) standard — one model per OKF revision, upstream of okf-tools.
-
Updated
Aug 28, 2026 - Shell
Private passport-compiled experiment domain for TMI-OS: guard dictionary, Lean 4 / Vampire / E build axis, controlled push surface.
-
Updated
Jun 24, 2026 - Shell
Binary-in-text encoding validation suite: uuencode, MIME Base64, XBM/XPM, X-Face, Ascii85, data URIs, org-mode. Literate FreeBSD test suite.
freebsd encoding base64 json-schema openapi mime property-based-testing literate-programming sdr formal-methods org-mode xbm ascii85 mtom basicode uuencode lean4 noaa-apt x-face
-
Updated
Apr 8, 2026 - Shell
Lean 4 CI: 3× faster Mathlib caching (Linux, containerized) with one-file workflow
bash github-pages cryptography verification reproducibility numerical-relativity lake github-actions lean4 cryptographic-manifests
-
Updated
Oct 12, 2025 - Shell
Created by Leonardo de Moura
Released 2013
- Followers
- 45 followers
- Repository
- leanprover/lean
- Website
- github.com/topics/lean
- Wikipedia
- Wikipedia