leanprover / lean4

Lean 4 programming language and theorem prover

leanprover-community / mathlib4

The math library of Lean 4

lean-dojo / LeanCopilot

LLMs as Copilots for Theorem Proving in Lean

google-deepmind / formal-conjectures

A collection of formalized statements of conjectures in Lean.

fabio-rovai / open-ontologies

Plan, apply and roll back changes to a production ontology, with a blast radius report and a proof an auditor can re-check.

h5i-dev / h5i

Unified Rust framework for building, verifying, and testing web apps. Kernel-based architecture for Lean 4 verification and GPU acceleration. Built-in red-teaming tools for automated vulnerability detection.

FloatingPragma / observer-patch-holography

Observer Patch Holography: finite observer consensus, machine-checked mathematics and reproducible models for reconstructing physical structure.

Julian / lean.nvim

Neovim support for the Lean theorem prover

leanprover-community / lean4game

Server to host Lean games

oOo0oOo / lean-lsp-mcp

Lean Theorem Prover MCP

morluto / jacobian

Composable mathematics tools for agents

1105216375-alt / resimind

Neuro-symbolic agents with verified memory. MCP math tools, an algebra repair Skill, and an open challenge. Verify solutions, learn checked rules, and reuse.

schildep / verified-3d-mesh-intersection

Formally verified 3D mesh intersection - trust 93 lines of spec, not 1000+ lines of AI-written code

lean-dojo / FloatLib

Arbitrary verified fast precision floating point arithmetic in Lean, with proofs, optimized backends, and support for IEEE binary and decimal, posits, and custom formats.

gaearon / conway-refinement

A proof of Conway's refinement conjecture in Lean

BasisResearch / ship-your-interpreter

Lean 4 + the Sail-generated RISC-V ISA model prove, CompCert-style, that an inductive WHILE semantics abstracts a real interpreter binary — zero sorries, zero axioms

amelieloher / math-paper-skills

Agent skills for writing research mathematics in LaTeX and building audited visual companion websites for papers.

ColinBundschu / mass-gap

The mass gap over the compact simple groups

infervisor / plow

Packet Language for On-device Warps — a GPU inference compiler and runtime

siqiliu-tsinghua / tautology

Real analysis formalized in Lean 4 from nothing — the reals are constructed here. No mathlib, no external dependencies, no typeclasses.

Swapnil-jain / integer-mult-kappa

Integer multiplication below n log n: a conditional witness kappa = 6685733/10^10 (> 2^-11) for T(n) = O(n (log n)^(1-kappa)) in the multitape model, building on OpenAI's problem and Colkitt's integer-mult-bounds: certificates, independent replays, Lean 4 checks