Oliver Dressler

Software engineer with a PhD from ETH Zürich. I build systems where software meets hard problems: AI for machine-checked mathematics in Lean 4, quantitative investment platforms and automated scientific instruments. These days I mostly build tools that let AI agents do real work: proving theorems in Lean, apps for ChatGPT and MCP servers.

Text versions: projects.html · projects.md · llms.txt

Software

Diorama: Describe a scene in ChatGPT and a 3D voxel diorama builds beside the chat.
Oliver's Anatomy: A 3D anatomy atlas in the browser: muscles, bones, nerves, vessels and organs, where pain can come from, and the body moving.
Lean Theorem Prover MCP: MCP that allows agentic interaction with the Lean theorem prover using leanclient.
Lean Scribe: VSCode extension for rendering and running context-rich Lean 4 prompts using state-of-the-art LLMs.
leanclient: Python client to interact with the lean4 language server.
Lean Tooling: Small open-source libraries and tools around Lean 4.
pynanite: Automatic level of details for 3D models.
Structure of Lean: Visualizing the proof structure in Lean and Mathlib.
Winery Map: Explore 90,000+ wineries in 95 countries on an interactive map.
Proof of Groove: We move together We groove together
Scrapsters: Sustainable Shopping with Scrapsters
The Pixel Democracy: Majority rules, period!
CoCrafty: Develop startup ideas. Easy. Together.

Work

Math, Inc.: Math, Inc. builds AI systems for machine-checked mathematics.
Human Edge: The next step in asset management.
Lecturing at FFHS: I lecture multiple courses at the Fernfachhochschule Schweiz, a university of applied sciences.
QuickPool by Ardeo: Ardeo is providing cutting edge shift planning solutions.
Winnie & Tack: Go on a hike and experience an interactive adventure with Winnie and Tack.
Digital Literacy: Strengthening digital opinion-forming with simulations.
PhD in Chemical Engineering: I completed my PhD in Chemical Engineering at the ETH Zurich.
Publications: A selection of publications written during my PhD: Reinforcement Learning for Dynamic Microfluidic Control; Continuous and low error-rate passive synchronization of pre-formed droplets; Doctoral Thesis

Games

Vector Flow: Casually roll balls towards enemies. Pick the correct position to eliminate all targets.
Infinitea: Do you feel like having a tea? Then this is the game for you.
Ready for Takeoff: Manage a small airport with your friends. Help passengers reach their destination.
Macro Mate: Multiplayer chess on a map!
Cinemoji: Think of a movie.
Rocket Kite: Fly your rocket kite among the planets.
Wiki Hike: Find the connection between two random articles on wikipedia. Keep moving forwards.
Cloud Tower: Build a tower of clouds and reach new heights in this small game.
Bite: A short game about a hungry vampire with water color art.
Scurry: Keep your rabbits save by whistling. Just chill and whistle...

Music

Soundtracks: A collection of over 50 short soundtracks for games, audio books and animations.
Proof of Groove: We move together We groove together
The Floating Seconds: For many years we have developed our unique blend of instrumental progressive rock.