Stars
The Seiberg-Witten solution of N=2 SU(2) super-Yang-Mills, formalized in Lean 4: physics as named postulates, machine-checked consequences, audited assumptions
A Lean 4 formalization of the Gaussian Free Field in d=4 and proof of the Osterwalder-Schrader axioms
|toqito> (Theory of Quantum Information Toolkit) is a Python library for research in quantum information theory.
Fast Lean 4 proof feedback for coding agents. CLI, Python library, and MCP server with warm LeanInteract sessions and cached env reuse.
A Lean formalisation of Maryna Viazovska's Fields Medal-winning solution to the sphere packing problem in dimension 8.
Meditron is a suite of open-source medical Large Language Models (LLMs).
A collection of formalized statements of conjectures in Lean.
gpt-oss-120b and gpt-oss-20b are two open-weight language models by OpenAI
A standard API for single-agent reinforcement learning environments, with popular reference environments and related utilities (formerly Gym)
Tools for constructing and analyzing quantum low density parity check (qLDPC) codes. Also stabilizer and subsystem codes more broadly.
Clifford circuits, graph states, and other quantum Stabilizer formalism tools.
A web-based collaborative LaTeX editor
A Julia library for Pauli propagation simulation of quantum circuits and quantum systems.
Krylov methods for linear problems, eigenvalues, singular values and matrix functions
A painfully slow Python demonstration of a Pauli transfer matrix simulator
a lightweight, open-source blueprint for building powerful and scalable LLM chat applications
Curated coding interview preparation materials for busy software engineers
Generate hierarchical quantum circuits for Neural Architecture Search.
A python package for Grassmann tensor network computation
Tensor network based quantum software framework for the NISQ era
Python package for compiling and analyzing quantum algorithms to simulate electronic structures.