# Oliver Dressler: Projects > 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 version of https://oli.show/, which renders the same content as an interactive 3D scene. HTML version: https://oli.show/projects.html. Raw data: https://oli.show/static/config.json. ## Software ### Diorama Describe a scene in ChatGPT and a 3D voxel diorama builds beside the chat. Ask for changes and it rebuilds in place. - ChatGPT app built on the Model Context Protocol (MCP). - The model writes a small scene language; the scene grows block by block. - Free, no account, on the web and on phones. Technologies: LLM, TypeScript, Three.js Link: [Build Now!](https://diorama.oli.show/) ### 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. - Tap where it hurts to see possible causes: trigger points, nerve roots, organs. - The body posed and moving with a physics model (MuJoCo). - Every number names its source. For education, not medical advice. Technologies: TypeScript, Three.js, WebAssembly Link: [Explore Now!](https://anatomy.oli.show/) ### Lean Theorem Prover MCP [MCP](https://modelcontextprotocol.io/introduction) that allows agentic interaction with the [Lean theorem prover](https://lean-lang.org/) using [leanclient](https://github.com/oOo0oOo/leanclient). - 500+ stars on GitHub. - Agentic interaction with the Lean theorem prover. - Enables querying goal states, hover information, and [leansearch.net](https://leansearch.net). - Supported in VSCode, Cursor, and across OSs. Technologies: Lean4, Python, LLM Link: [Interact Now!](https://github.com/oOo0oOo/lean-lsp-mcp) ### Lean Scribe VSCode extension for rendering and running context-rich Lean 4 prompts using state-of-the-art LLMs. - Render context-rich prompts using the current open Lean 4 file. - Query multiple state-of-the-art large language models. - Define prompts as shareable markdown files with Jinja templating. Technologies: VSCode Extension, Lean4, TypeScript Link: [Prompt Now!](https://github.com/oOo0oOo/lean-scribe) ### leanclient Python client to interact with the lean4 language server. - Interact: Query and change lean files via the LSP. - Fast: Typically more than 99% of time is spent waiting. - Parallel: Easy batch processing of files using all your cores. Technologies: Lean4, Python Link: [Interact Now!](https://github.com/oOo0oOo/leanclient) ### Lean Tooling Small open-source libraries and tools around [Lean 4](https://lean-lang.org/). - [LeanDoomed](https://github.com/oOo0oOo/LeanDoomed): a raycasting game written in Lean with SDL3. - [LeanSage](https://github.com/oOo0oOo/LeanSage): SageMath integration for Lean. - [LeanSerde](https://github.com/oOo0oOo/LeanSerde) (type-safe serialization) and [LeanRPC](https://github.com/oOo0oOo/LeanRPC) (Lean functions over HTTP). - [LeanParanoia](https://github.com/oOo0oOo/LeanParanoia): proof verification without a reference. - [mathmux](https://github.com/oOo0oOo/mathmux): a CLI for parallel agent work on Lean projects. Technologies: Lean4, C, Python Link: [Browse Now!](https://github.com/oOo0oOo?tab=repositories&q=lean) ### pynanite Automatic level of details for 3D models. Implementation in Python based on Unreal Engine's LOD system. - Automatic level of details for 3D models without artist input. - Relatively performant for a Python implementation. - Algorithm based on graph partitioning. Technologies: Python, Scipy et al., Rendering Link: [Render Triangles Now!](https://github.com/oOo0oOo/pynanite) ### Structure of Lean Visualizing the proof structure in Lean and Mathlib. - Visualizes the dependencies of lean4 and mathlib4 proofs on a theorem level. - Interactive graph visualization using sigma.js. - Static website, all content is loaded at page load. Technologies: Svelte, Lean4, sigma.js Link: [Visualize Now!](https://oli.show/leanstructure/) ### Winery Map Explore 90,000+ wineries in 95 countries on an interactive map. Find your next wine tasting destination! - 2,786 appellations and 43,000 km² of vineyards from 333 open sources. - Filter by organic, grape and price; a page for every region. - Fast on phones: vector tiles read in small pieces (PMTiles). Technologies: TypeScript, Maps, Data Science, Browser Link: [Taste Now!](https://wine.oli.show/) ### Proof of Groove We move together We groove together Proof of Groove is an NFT, generated using a fully decentralized synthesizer. - Uses a [custom subgraph](https://thegraph.com/docs/en/developing/assemblyscript-api) to create NFTs fully decentralized. - Each NFT is a unique SVGs with embedded raw WAV signals. - Complete procedural generation in WebAssembly. Technologies: Music, WebAssembly, Solidity, React ### Scrapsters Sustainable Shopping with Scrapsters Winning project for the HackZurich 2023 Migros challenge! - A sustainable Migros MANIA. - Kids can upcycle packaging into toys, decorated with QR code stickers. - The QR codes lead to custom generated audiobooks about this scrapster. Technologies: Upcycling, Vue.js, Flask, LLM Link: [Devpost](https://devpost.com/software/scrapsters) ### The Pixel Democracy Majority rules, period! Collaborative drawing board. You decide where the line goes next! Technologies: Flask, JavaScript, Socket.io Link: [Draw Now!](https://pixel.oli.show/) ### CoCrafty Develop startup ideas. Easy. Together. CoCrafty is a collaboration platform for developing startup ideas. - A variety of collaborative real-time tools: Mind-mapping, chat, ... - No longer actively maintained. Use it while it's still online! Technologies: Flask, JavaScript, Cloud, Socket.io Link: [Collaborate Now!](http://cocrafty.com/) ## Work ### Math, Inc. [Math, Inc.](https://math.inc/) builds AI systems for machine-checked mathematics. As a Founding Research Engineer I worked on large-scale autoformalization in [Lean 4](https://lean-lang.org/). - Agent tooling for AI-assisted formalization of mathematics. - Evaluation pipelines for machine-checked proofs at scale. Technologies: Lean4, LLM, Python Link: [Formalize Now!](https://math.inc/) ### Human Edge The next step in asset management. Human Edge provides systematic investment solutions. - Responsible for technical decisions and architecture (CTO). - Train machine learning models for investment strategies. - Develop and maintain our Flask-based web app. Technologies: Scipy et al., Machine Learning, Cloud Link: [Invest Now!](https://www.human-edge.ch/) ### Lecturing at FFHS I lecture multiple courses at the Fernfachhochschule Schweiz, a university of applied sciences. My focus is on applications of large language models, blockchain technology and software development in general. - Lecturing on practical applications of LLMs. - Teaching technical aspects of blockchain technology. Technologies: LLM, Blockchain, Solidity Link: [Learn Now!](https://www.ffhs.ch/en/ffhs/people-finder/person/dressler-oliver) ### QuickPool by Ardeo [Ardeo](https://ardeo.ch) is providing cutting edge shift planning solutions. I support them as a freelancer with software development and technical decisions. - Developed shift validation system. - Integrated and customized automatic shift planning. Technologies: Angular, Ruby, Clojure, Machine Learning Link: [Optimize Now!](https://quickpool.ch/) ### Winnie & Tack Go on a hike and experience an interactive adventure with Winnie and Tack. Listen to the audio book and make your own decisions. - Two adventures available, two new ones coming soon! - Cross-platform app released on [Android](https://play.google.com/store/apps/details?id=ch.abenteuerweg.adventure) and [iOS](https://apps.apple.com/us/app/abenteuerweg-mit-winnie-tack/id1558362365). - During the adventure no internet connectivity is required. Technologies: Unity, Android, ios, csharp Link: [Experience Now!](https://abenteuerweg.ch/) ### Digital Literacy Strengthening digital opinion-forming with simulations. Developed with [Dezentrum](https://www.dezentrum.ch/en/) and the [Risk Dialogue Foundation](https://www.risiko-dialog.ch/en/). - Experience online phenomena and risks in this simulation. - Real-time chat using socket.io. - Simple access to simulations via link. Technologies: Flask, Vue.js, Socket.io, Cloud Link: [Discuss Now!](https://www.digital-literacy.live/) ### PhD in Chemical Engineering I completed my PhD in Chemical Engineering at the ETH Zurich. My research focused microfluidic technology and how to control it using machine learning. - Droplet microfluidics using lab-on-a-chip devices. - Application of reinforcement learning from image data for real-time microfluidic control. - 3D-printing of fluidic structures for larger scale devices. Technologies: Microfluidics, Machine Learning, Python Link: [My Publications](https://oli.show/projects.html#work_publications) ### Publications A selection of publications written during my [PhD](https://oli.show/projects.html#work_phd): - [Reinforcement Learning for Dynamic Microfluidic Control](https://pubs.acs.org/doi/10.1021/acsomega.8b01485) - [Continuous and low error-rate passive synchronization of pre-formed droplets](https://pubs.rsc.org/en/content/articlelanding/2015/ra/c5ra08044d) - [Doctoral Thesis](https://www.research-collection.ethz.ch/handle/20.500.11850/269520) - Droplet microfluidics using lab-on-a-chip devices. - Application of reinforcement learning from image data for real-time microfluidic control. Technologies: Microfluidics, Machine Learning, Python Link: [All Publications](https://www.researchgate.net/scientific-contributions/Oliver-J-Dressler-2036925851) ## Games ### Vector Flow Casually roll balls towards enemies. Pick the correct position to eliminate all targets. Unlock specials to increase your chances! - Patchinko with enemies! - Required lots of level design. Technologies: Godot, Android, HTML5 Link: [Flow Now!](https://code-box.itch.io/vector-flow) ### Infinitea Do you feel like having a tea? Then this is the game for you. Just keep on brewing! Our try at an incremental game. Technologies: JavaScript, Browser Link: [Brew Now!](https://oli.show/tea/) ### Ready for Takeoff Manage a small airport with your friends. Help passengers reach their destination. This real-time, multiplayer game requires a lot of teamwork! - Real-time multiplayer using Godot remote procedural calls. - A server (also coded in GDScript) runs all current instances of the game. Technologies: Godot, Cloud, Android Link: [Fly Now!](https://play.google.com/store/apps/details?id=com.slingshotmedia.readyfortakeoff) ### Macro Mate Multiplayer chess on a map! Proof of concept for a single player (+ bots) version of the game. - Many more game states than chess. - Required heavy [simplifications](https://github.com/oOo0oOo/macromate#bots) to make an AI feasible. - Tree search with alpha-beta pruning. Technologies: Python, Scipy et al. Link: [Play Now!](https://github.com/oOo0oOo/macromate) ### Cinemoji Think of a movie. I will guess your movie based on emojis. - Use ChatBot for "level" [generation](https://github.com/oOo0oOo/cinemojis/blob/main/scripts/emojify.py#L28). - No API calls needed during play. - Suggest emojis based on likely movies. Technologies: LLM, TypeScript, Browser Link: [Try Now!](https://oli.show/cinemoji/) ### Rocket Kite Fly your rocket kite among the planets. Use gravity and collect all checkpoints. - Multi-body physics simulation. - Monochrome with varying color schemes. - Published for Android using buildozer. Technologies: Python, Kivy, Android Link: [Fly Now!](https://play.google.com/store/apps/details?id=rocketkite.rocketkite) ### Wiki Hike Find the connection between two random articles on wikipedia. Keep moving forwards. There are quite a few surprising links. - Required reducing the complete simple wikipedia down to 4.2MB of adjacencies. - User downloads the complete data set. - Game runs locally in the browser. Technologies: JavaScript, Browser Link: [Hike Now!](https://oli.show/wikihike/) ### Cloud Tower Build a tower of clouds and reach new heights in this small game. First Godot game published on Android. Technologies: Godot, Android Link: [Stack Now!](https://play.google.com/store/apps/details?id=org.godotengine.towermaster) ### Bite A short game about a hungry vampire with water color art. Drink enough blood to survive 2 years. Don't kill the parents. Technologies: Painting, JavaScript, Browser Link: [Drink Now!](https://oli.show/bite/) ### Scurry Keep your rabbits save by whistling. Just chill and whistle... Developed for a [game jam](https://itch.io/jam/trijam-123/rate/1071357) using Godot. - Developed in 15h. - Custom soundtrack: [Rabbit Bop](https://freesound.org/people/code_box/sounds/575759/). Technologies: Godot, HTML5, Ableton Live Link: [Whistle Now!](https://code-box.itch.io/scurry) ## Music ### Soundtracks A collection of over 50 short soundtracks for games, audio books and animations. Composed and rendered using Ableton Live. Free download available on freesound.org. - All tracks are released to the public domain under [CC0](https://creativecommons.org/share-your-work/public-domain/cc0/). - Variety of styles, whatever I feel like :D Technologies: Music, Ableton Live Link: [Listen Now!](https://freesound.org/people/code_box/) ### Proof of Groove We move together We groove together Proof of Groove is an NFT, generated using a fully decentralized synthesizer. - Uses a [custom subgraph](https://thegraph.com/docs/en/developing/assemblyscript-api) to create NFTs fully decentralized. - Each NFT is a unique SVGs with embedded raw WAV signals. - Complete procedural generation in WebAssembly. Technologies: The Graph, WebAssembly, Solidity, React ### The Floating Seconds For many years we have developed our unique blend of instrumental progressive rock. Unfortunately this band is no longer active but you can still listen to our music for free on Soundcloud. In this live recording I was playing synth and was involved with composition and 'mastering'. Technologies: Synth, Ableton Live, Drums Link: [Listen Now!](https://soundcloud.com/thefloatingseconds/sets/satans-bbq-at-mehrspur) ## About ### Biography Hi, I am 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](https://lean-lang.org/), 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. Located in Switzerland. Check out my current [work](https://oli.show/projects.html#work). ### This Page Solar system 3D portfolio page. Let me know if you find any bugs ;-) - Interactive 3D visualization using three.js. - Easily configurable using [JSON](static/config.json). - Text versions for search engines and AI agents: [HTML](projects.html), [Markdown](projects.md) and [llms.txt](llms.txt). Technologies: TypeScript, Three.js Link: [Repository](https://github.com/oOo0oOo/personalpage) ### Contact Work inquiries (freelance, contract, advising): [work@oli.show](mailto:work@oli.show) Quick questions: write to [notquiteoliver.01](https://signal.me/#eu/D0UDRjo6cTHMOHcPG6fT2-EjoXjA_5vzpsybGPidlw2cEn61xPlGdrExAYpLPO_b) on Signal (scan the code). [Not Quite Oliver](https://oli.show/assistant/) is my AI assistant: it answers first and passes everything on to me. Anything else: [hey@oli.show](mailto:hey@%6Fli.show)