Grid-Free Monte Carlo Solvers for Physics Simulations Involving Partial Differential Equations

A prompt engineering functional programming language

Universal Notation for Tensor Operations in Python

Synthetic Tait computability in intensional type theory

A search program used to optimize the Snarkmaker

Machine-checked Agda formalisation of the canonical normal form theorem for the type theory of regular categories

Ground Zero: Lean 4 HoTT Library

100M tokens. Infinite compute. Lowest val loss wins.

A platform for formalizing OEIS sequences in Lean 4

A new extraction system from Rocq to functional-style, memory-safe, thread-safe, readable, valid, performant, and modern C++.

A plain text-based spaced repetition system.

A collection of optimization problems in mathematics

A modern, principled toy implementation of dependent type theory

Fast equality saturation in Haskell

Extensions to cubical for categorical logic/type theory

This repository contains companion software for the Colfax Research paper "Categorical Foundations for CuTe Layouts".

Experimental library for Narya

A tutorial on how Agda infers things

being bits and pieces I'm inclined to leave lying around

Staged compilation with dependent types

Trying to find the highest-scoring Boggle board with a mix of C++ and Python

CaDiCaL SAT Solver

A Low Barrier Proof Assistant

TeXpresso: live rendering and error reporting for LaTeX