ATLAS Autoformalized Textbook Library At Scale

Templates for getting started with Verso

Helper files for making math textbooks lean companions

A Lean 4 companion to Lawvere and Schanuel's Conceptual Mathematics (2nd ed)

Lean Companion to Axler's Linear Algebra Done Right

A Lean formalization of a bound concerning long gaps between primes

A proof of Conway's refinement conjecture in Lean

LeanArchitect extracts a blueprint directly from Lean source.

The math library of Lean 4

My solutions to Tao's Analysis I, formalized in Lean

Claude Code skill: navigator protocol for building code or proofs together, where you drive and Claude guides you to do it alone

An AIs-welcome Lean library downstream of Mathlib: AI handle the implementation and review, humans write the roadmaps and review rubrics

WikiLean — Wikipedia mathematics annotated with Mathlib4/Lean formalization links

Build iOS apps with Lean

Website for NYC Lean (lean.nyc)

Run lean4 directly in your browser ( https://lean.cau.li )

TopNotch is a lil Swift package that lets you hide a custom view underneath the device’s notch.

Python package for safe quantum programming that compiles to Qiskit, where the type system enforces coherence and ancilla cleanliness

Agent skill for comprehensive ios codebase audit

iOS app for posting SOOC photos with web admin panel

Example for connecting Linear Agents SDK with Claude Managed Agents

Performant and reusable text view component (TextKit 2), with line numbers and more. UITextView / NSTextView replacement.

Publish a Day One journal as a static site. Easily make a sharable, publicly-viewable travel blog, baby photo album, or anything else.

A formal proof of the Riemann Hypothesis for curves