A set of ready to use scientific skills for Claude

A game introducing proofs, dependent type theory, and Lean prepared for a first year seminar course at Johns Hopkins in Fall 2025.

Algorithmic Information Theory, using Binary Lambda Calculus

two basic results on absolutely continuous functions

Structured data extraction and programmatic interaction with Lean 4.

Minimal open-source implementation of AlphaProof [WIP]

A recursive, reflective POETRY algorithm variant using Goedel-Prover-V2

Recursive LLMs for Retrosynthesis

Formalize the construction of the ismorphism from l1 (the space of summable sequences over the real numbers) to the dual space of c0 (the space of sequences converging to 0 endowed with sup norm)

This file formalized that if $R$ is noetherian, then its power series ring $R[[X]]$ is also noetherian

A drawing utility for unit-distance and related embeddings of graphs

Prover Agent: An Agent-Based Framework for Formal Mathematical Proofs

Formally proving the security of Fast Reed-Solomon interactive oracle proofs of proximity

Running Aristotle from Harmonic on Putnam 2025 problems

This repository allows reproduction of Poetiq's record-breaking submission to the ARC-AGI-1 and ARC-AGI-2 benchmarks.

A formalization of the Banach-Tarski theorem in Lean

Bounding sphere mathematics in Lean. Contains a proof of Jung's theorem https://en.wikipedia.org/wiki/Jung%27s_theorem

Leaff is a diff tool for Lean environments

yet another 2048, but this time it's controlled by GPT

N-Tuple Networks for the Game 2048 in Python

A simple Bench for 2048

LLM/VLM gaming agents and model evaluation through games.

I created a simple GUI page for the yt-dlp project.