Python utilities for loading and working with the FormulationBench dataset. FormulationBench is a collection of 20 optimization problems with 109 mixed-integer linear programming (MILP) formulations. Each formulation has a natural language description, LaTeX formulation, GurobiPy implementation, and Lean representation. Furthermore, there are 89 pairs of formulations consisting of 63 positive reformulation examples and 26 negative examples. Each positive example has a machine-checked Lean 4 reformulation proof. See the documentation for details.

OpenATP is an open-source Python package providing a common interface for automated theorem proving (ATP). OpenATP focuses on recent agentic ATP methods that prove formal statements in Lean. Each method runs in an isolated sandbox, either locally with Docker or remotely with Modal. OpenATP also provides benchmarking utilities to run methods on common datasets.

Supported ATP methods include: Claude Code, Codex, DeepSeek, Grok, Muse Spark, AxProverBase, Leanstral, Kimi Code, Numina, and Aristotle. See the documentation for an up-to-date list.

I really like live music. I’ve been tracking the shows I attend on a personal website for several years. Recently, I created showcount.com, a website for tracking and sharing concert attendance. It has all the bells and whistles as my prior website, but anyone can make an account and share their list with friends.

I’m aware there are many other concert and setlist tracking websites (Phantasy Tour, Concert Archives, Songfish, Setlist.fm). I built showcount because I wanted full creative control and full access / ownership of my data. I also didn’t want to manually upload my shows to one of the other platforms — showcount has a built-in AI import option that parses arbitrary data formats.

This was also my first experiment with vibe-coding and harness-engineering (see my HN Post).

llamda (LLm AutoMatically Designed Algorithms) is a Python package for LLM-based automatic heuristic design. An LLM proposes candidate heuristics as Python code, each candidate is evaluated on a benchmark of instances, and an evolutionary search algorithm guides the generation of new candidate heuristics.

The package provides a single interface over several published methods (FunSearch, EoH, ReEvo, HSEvo, and MCTS-AHD) so that they can be run and compared on common ground. It also includes common combinatorial optimization problems: traveling salesman problem (TSP), capacitated vehicle routing (CVRP), bin packing (online and offline), and the multiple knapsack problem.

simpar (SIMulate PAndemic Response) simulates the spread of a disease through a heterogeneous population using an SIR model. The groups module can be used to manage a heterogeneous population comprised of “meta-groups” with varying contact levels. The tool focuses on providing functionality for assessing pandemic response strategies such as isolation protocols, testing regimes (with varying tests), and vaccination requirements. The Strategy class is used to define a potential strategy. The Scenario class is used to manage the parameters pertaining to a scenario under which a disease is spreading. This consists of a population, environment parameters (e.g. outside rate of infection), and disease parameters (e.g. symptomatic rate). Lastly, the Trajectory class offers methods to compute metrics on a simulation of some strategy applied to a scenario. For more details, see the Documentation.

cotat is a visualization tool for the analysis of contact tracing data. Given a dataframe of people (along with their attributes) and a dataframe of known contacts among the individuals, cotat exports an interactive HTML visualization of the network. Furthermore, certain columns of the people dataframe can be labeled as “membership columns” which allows one to visualize which people belong to the same groups (e.g. building, club, etc..) even if a contact between those individuals has not been reported.

dmtools (Digital Media Tools) is a Python package providing low-level tools for working with digital media programmatically. The netpbm module allows one to read and create Netpbm images. Color space transformations can be done with the colorspace module. Using ffmpeg, the animation module can export .mp4 videos formed from a list of images and the sound module can be used to add sound to these videos as well. Lastly, ASCII art can be produced with the ascii module.

All Things Umphrey’s (ATU) is the static website which maintains setlist data for Umphrey’s McGee. This project provides functionality to scrape setlist data from ATU and compile a Deadbase-style book affectionately referred to as Umphbase.

Initially, Selenium and Beautiful Soup were used to scrape the data from the site. However, in June of 2021, a new version of ATU was released which provides an API to access the site’s data. Read more about the transition here. The TL;DR is the new version is based on a setlist engine called Songfish by Adam Scheinberg.

vinal is a Python package for visualizing graph/network algorithms. Currently, the following algorithms are implemented:

• Shortest path problem
  • Dijkstra’s algorithm
• Minimum Spanning Tree (MST)
  • Prim’s Algorithm
  • Kruskal’s Algorithm
  • Reverse Kruskal’s Algorithm
• Travelling Salesman Problem (TSP)
  • Random neighbor
  • Nearest neighbor
  • Nearest insertion
  • Furthest insertion
  • 2-OPT

NetworkX graphs can be constructed from a single .csv file of node locations. Alternatively, one can specify edges of the graph by providing an additional .csv file of edges. The package relies on bokeh to generate standalone HTML files which can be viewed in a Jupyter Notebook inline or in a web browser.

GILP (Geometric Interpretation of Linear Programs) is a Python package for visualizing the geometry of:

• Linear Programs (LPs)
• The Simplex Algorithm
• The Branch and Bound Algorithm

LPs can be constructed from NumPy arrays and many examples (such as the Klee-Minty cube) are included. The revised simplex method is implemented along with phase I for finding an initial feasible solution. The package relies on Plotly to generate standalone HTML files which can be viewed in a Jupyter Notebook inline or in a web browser.

Graph Builder is a Java program for constructing graphs. It currently supports undirected, directed, and structural graphs. Additionally, the “Grid Graph” selection allows for creating graphs where node positions are locked on to a grid. The following graph statistics are maintained as the graph is constructed.

• Node count (int)
• Edge count (int)
• Connected (bool)
• Smallest and largest degree (int)
• Average degree (float)
• Smallest and largest geodesic (int)
• Average geodesic (float)

Additionally, the list of each node’s neighbors is maintained.