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
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.
cuda-oxide is an experimental Rust-to-CUDA compiler that lets you write (SIMT) GPU kernels in safe(ish), idiomatic Rust. It compiles standard Rust code directly to PTX — no DSLs, no foreign languag…
Lightweight Sandbox Powered by a Purpose-Built VM and OS
Verified computational algebra in Lean 4 — polynomial factoring, LLL, and friends
Use Claude Code's autonomous agent loop with DeepSeek V4 Pro, OpenRouter, or any Anthropic-compatible backend. Same UX, 17x cheaper.
SMTscope automatically analyses and visualises SMT solver execution traces.
Simply add icons to anything you want in Obsidian.
A theoretical reconstruction of the Claude Mythos architecture, built from first principles using the available research literature.
property testing and verification front-end for Rust
A high-performance FIX (Financial Information Exchange) protocol encoder/decoder written in Rust
Highlight and capture the web in your favorite browser. The official Web Clipper extension for Obsidian.
Single-pass SSA bytecode compiler and threaded-code stack VM for a sandboxed Python subset: NaN-boxed values, inline caching, super-instruction fusion, pure-function memoization, mark-sweep GC. Cov…
A writing workflow using Scrivener's style system + Pandoc for output…