The Lean research ecosystem, in one directory.

A repository for participation in the LeanLang for Autonomy Hackathon held from April 17 to May 01, 2026 at Indian Institute of Science, organised by Emergence AI.

Plonky3 formal verification framework

Proof-of-Concept Verification Infrastructure for SP1 zk chips

Construction of a flow equivalent forest from a flow matrix in Lean 4

Tiny Lean library to check existence of declarations

It is a windows folder explorer written in lean4 (using code-proxy).

Formalising the Ring of Integers in Quadratic Fields in the Lean proof assistant.

elementary number theory

A set of tools and extensions for Lean

Terminal colors and styling for Lean 4

Minimal static analysis based verifier for educational purpose

Tools, specifically for running tactics in the background, with minimal dependencies

The proof that the adele ring of a number field is locally compact, formalised in Lean 4.

Formalising non-commutative graph theory in Lean

A Lean 4 library for analyzing Spin Point Groups

A 12-primitive measurement apparatus for the structural type of any system - 17,280,000-address Crystal of Types

Formal verification of knowledge soundness for Generalized Bulletproofs

Verified HTTPS server in Lean 4 - TLS 1.3, HTTP/2, QUIC, WebSocket, gRPC - 914 machine-checked theorems, zero sorry. Pure library available (LeanServerPure).