Lists (16)
Computer Algebra
Computer algebra tools12 repositories
Dependent Types
Dependent type checking2 repositories
E-Graphs
Equality saturation is a technique for building optimizing compilers using e-graphs16 repositories
Geometric Algebra
Geometric algebra is a mathematical framework that unifies and extends vector algebra5 repositories
HEP
High energy particle physics3 repositories
JIT Compilers
JIT compilers are a type of compiler that translates code into machine code at runtime, improving performance by optimizing code15 repositories
Lean
Lean theorem prover29 repositories
MCP
Model Context Protocol11 repositories
MLIR
MLIR (Multi-Level Intermediate Representation) is a unifying software framework for compiler development.15 repositories
Physics
Uncategorized physics projects7 repositories
Quantitative Finance
Study of market structure using quantitative models3 repositories
Reasoning Models
Language models that enumerate stepwise before answering.11 repositories
SMT Solvers
Satisfiability modulo theories19 repositories
Tensor Calculus
Symbolic tensor calculus manipulation tools10 repositories
Term Rewriting
5 repositories
Zero Knowledge Proofs
1 repository
Starred repositories
WikiLean — Wikipedia mathematics annotated with Mathlib4/Lean formalization links
Kimi Code CLI is your next CLI agent.
⛔ A lightweight website blocker with a user friendly interface
Programming language for literate programming law specification
A functional, content-addressable programming language.
Aspects of categorical differential geometry, formalised in lean 4.
A neovim plugin for folding documentation comments in rust files.
Insert is a programming language for self-modifying code.
(at least a useful portion of) Temporal Logic of Actions, a.k.a. TLA in Lean 4
[SIGMOD 2026] F3: The Open-Source Data File Format for the Future
Wasm interpreter in lean, designed for reasoning
BRAT - Beta Reviewer's Auto-update Tool for Obsidian.
A Rust implementation of interval arithmetic (IEEE 1788)
SQLite extension + bindings for Postgres NOTIFY/LISTEN semantics with durable queues, streams, pub/sub, and scheduler
For developing and reproducing ML + HEP projects.
Prover9 is a resolution and paramodulation-based theorem prover for first-order and equational logic, and Mace4 searches for finite counterexamples.