Starred repositories
A project to digitalise results from physics into Lean.
A collaborative Lean 4 formalization of Mazur's torsion theorem
An AIs-welcome Lean library downstream of Mathlib: AI handle the implementation and review, humans write the roadmaps and review rubrics
SpaceXAI's coding agent harness and TUI. Fullscreen, mouse interactive, extensible.
Lightweight coding agent that runs in your terminal
👻 Ghostty is a fast, feature-rich, and cross-platform terminal emulator that uses platform-native UI and GPU acceleration.
Functional programming language for signal processing and sound synthesis
OBLITERATE THE CHAINS THAT BIND YOU
Open source Ghostty-based macOS terminal with vertical tabs and notifications for AI coding agents. Built for multitasking, organization, and programmability.
A Lean4 script for robustly verifying submitted proofs of theorems and implementations of functions
A collection of optimization problems in mathematics
Warcraft III Peon voice notifications (+ more!) for Claude Code, Codex, IDEs, and any AI agent. Stop babysitting your terminal. Employ a Peon today.
A Lean tactic for Canonical, a search procedure for terms in dependent type theory.
Python client to interact with the lean4 language server.
A collection of formalized statements of conjectures in Lean.
Canonical is a performant sound and complete type inhabitation solver for dependent type theory.
Lean 4 programming language and theorem prover
Next Generation Visual Programming System
A Stable ABI for Rust with compact sum-types