Stars
Claude Opus 4.6 wrote a dependency-free C compiler in Rust, with backends targeting x86 (64- and 32-bit), ARM, and RISC-V, capable of compiling a booting Linux kernel.
⚙️🗑️ A GitHub Action to free disk space on an Ubuntu runner.
A small collection of formally verified junk theorems provable in Lean4 + Mathlib.
Construction of a Brownian Motion in Lean
GitHub action that adds a label once a PR has merge conflicts
a zero-knowledge proof-carrying code platform for Lean 4
Ongoing project to formalise The Spectral Theorem in Lean prover
A collection of formalized statements of conjectures in Lean.
PDF++: the most Obsidian-native PDF annotation & viewing tool ever. Comes with optional Vim keybindings.
Computation verified by generating proof terms
🎬 A reactive (or non-blocking, or asynchronous) JSON parser
Library implementing type inference/checking functionality based on the Lean theorem prover
TensorZero is an open-source LLMOps platform that unifies an LLM gateway, observability, evaluation, optimization, and experimentation.
A translation framework for eliminating definitional equalities in Lean
A chrome extension to sync Amazon order details to Monarch
A project to map out the relations between different equational theories of Magmas.
Ongoing Lean formalisation of the proof of Fermat's Last Theorem