An auto-active verifier embedded into Lean

Match compilation algorithm in OCaml

Lean 4 formalization of arXiv:2603.21852 — All elementary functions from a single binary operator eml(x,y) = exp(x) - ln(y)

Lean4 library for substitution inspired by autosubst

Remote Control for Codex.

A Lean4 Formalization of Principles of Mathematical Analysis.

Lean 4 formalization of Rubik's cubes

Terminal based IDE & text editor: easy, powerful and fast

Lean 4 formalization of De Giorgi-Nash-Moser theory

Transforms complex documents like PDFs and Office docs into LLM-ready markdown/JSON for your Agentic workflows.

Lean theorem proving interface which feels like pen-and-paper proofs.

MathCode: A Frontier Mathematical Coding Agent

Manual segmented stacks for Rust

SciPy library main repository

A Textual widget for beautiful diffs in the terminal

Burn is a next generation tensor library and Deep Learning Framework that doesn't compromise on flexibility, efficiency and portability.

The 1SubML programming language - unified module and value language, structural subtyping, global type inference, higher rank polymorphic types, existential types, higher kinded types (no partial a…

Typed CSS AST, parser, pretty-printer, and optimiser for OCaml

A fast, safe, and intuitive DataFrame library.

async fn(Request) -> Result<Response, Error>

The Haskell Lightweight Virtual Machine (HaLVM): GHC running on Xen

Fast, accurate & comprehensive text measurement & layout

Direct-style parser combinator library for OCaml 5

Awesome Large Language Models for Vulnerability Detection

Property-based testing for Rust, built on Hypothesis

Notes (and implementation) of unification with binders

MCP, CLI, Skills for searching and downloading academic papers from multiple sources like arXiv, PubMed, bioRxiv, etc.

Adds MCP server to Blockbench