Building Bourbaki: A Math Agent That Can Check Its Own Work
How I built an autonomous agent for mathematical reasoning with SymPy, Lean 4, and structured proof techniques, and what I learned along the way
Yad Konrad
Applied researcher, comedian. Deep interest in meta problem solving, making machines write code that write code.
Recent Notes
View all →Make an Honest Resume for Your Coding Agent
Why giving your coding agent an honest map of what you know and don't know changes everything about how it helps you
Building Erdős Navigator: Claude Code as a Theorem Proving Assistant
How program synthesis led me down a rabbit hole through HoTT and algebraic topology, and back out through LLMs and a toolkit for 1,179 unsolved math problems
The Missing Toolbox: Civil Engineering, Ethics, and Creative Writing Classes
Why agent builders need lateral thinking from civil engineering, creative writing, and ethics
OWASP Top 10 for LLMs: A Pentester's Guide to Attacking and Defending
How to not get pwned building with LLMs. A red teamer's take on the new threat landscape.
Agent Sandboxes and the Proxmox Rabbit Hole
How my obsession with home labs led me to understand why coding agents need isolation
Featured Projects
View all →Hopper
AI coding assistant built in 2017 - before LLMs. Issue labeling, duplicate detection, commit generation using seq2seq.
Python Deep Learning NMT
Library of Comedy
The largest collection of standup comedy specials on the internet.
Python YouTube API Web Scraping
Nvidia-Autopilot-Keras
End-to-end self-driving neural network in Keras.
Keras TensorFlow Computer Vision