Formalization

Formalization projects in Lean 4.

Agent Foundations

Formalized Agent Foundations is my ongoing project formalizing results from agent foundations papers in Lean 4.

Papers so far: "Robust Cooperation in the Prisoner's Dilemma" and "Logical Induction".

Mathlib

I contributed the foundations of polygon geometry to Mathlib in two merged pull requests: #34393, defining polygons, and #34598, adding nondegeneracy conditions and interconversion with triangles.

Lean-Eval

I have had both problem and solution submissions accepted to the official Lean Eval for AI models. My solution submissions are housed in this repository, and my problem submissions can be found in my fork of the lean-eval repo.

About

This animation is generated by a turmite, a Turing machine that lives on a grid. Each step, the ant turns left or right depending on the color of its cell, increments that color, and moves forward one cell. The rule LR produces Langton's ant, and the numbered rules come from Further Travels with My Ant by Gale, Propp, Sutherland, and Troubetzkoy. Some rules build highways, some make symmetric mandalas, and some just make a mess. This page also runs the same rules on a hexagonal lattice. Click and drag to paint cells in the ant's path.