Oliver Dressler

lean-lsp-mcp. Lean Theorem Prover MCP

leanclient. Python client to interact with the lean4 language server.

LeanDoomed. Simple Raycasting Example in Lean4 using SDL3

RocketKite. Fly around the planets in this space simulator (kivy, Android)

winerymap. Map showing 34k wineries from all over the world.

LeanSage. SageMath integration for Lean4

lean-scribe. Render and run context-rich Lean 4 prompts in VS Code.

LeanSerde. Type-safe serialization for Lean

DrumMachine. Using WaveNet to create drum samples

LeanRPC. Serve Lean 4 functions as RPC methods over HTTP

LeanParanoia. Lean 4 proof verification without reference

teas. JavaScript

CloudTower. A 2D stacking game made using the Godot game engine

ReadyForTakeoff. Multiplayer, cooperative mobile game made using Godot Engine.

lean-lsp-mcp-numina. Python

PlanetDate. A simple website showing the current date (AD) on other planets

MapGenerator. A Random Map Generator for MapWarfare type strategy games

ValveController. A Python Interface for a USB I/O-based Solenoid Valve Controller

DeepnoteCpp. Render a THX deep note using C++

leanstructure. Visualize dependencies of lean4 proofs