Code for "Baba Is AI: Break the Rules to Beat the Benchmark"

Single-cell analysis in Python. Scales to >100M cells.

Trainable, memory-efficient, and GPU-friendly PyTorch reproduction of AlphaFold 2

Academic CVs that you can emulate

Hand-written verified Lean solutions for the HumanEval benchmark

CLEVER: Code Lean Evaluation for Verified End-to-end Reasoning

Canonical is a performant sound and complete type inhabitation solver for dependent type theory.

Experiments on automation for Lean

A prototype for a monadic program logic in Lean that has since been upstreamed into the Lean 4 repo

A project to digitalise results from physics into Lean.

The official repository for the paper Multilingual Mathematical Autoformalization

An updated version of miniF2F with lots of fixes and informal statements / solutions.

A Rocq version of the miniF2F dataset

Intuitive, type-safe expression quotations for Lean 4.

GitHub Action for the OCaml programming language

cvc5 is an open-source automatic theorem prover for Satisfiability Modulo Theories (SMT) problems.

Type Checking in Lean 4

👀 dynamically interact with vim registers

A tool for cleaning up unused Lean toolchains

computable implementation of real numbers in Lean4

A jq clone focussed on correctness, speed, and simplicity

Complexity analysis in Lean

(Mirror) A Machine-to-Machine Interaction System for Lean 4

Metaprogramming, verified meta-theory and implementation of Rocq in Rocq

The Lean reference manual

Code related to the Lean verification of the empty hexagon theorem

A deprecated equality saturation tactic for Lean based on egg.

A Machine-to-Machine Interaction System for Lean 4.

Tactics for discharging Lean goals into SMT solvers.

A Foreign Function Interface (FFI) to cvc5 solver in Lean.