Posts

Learning Lean 4 and Dependent Types

Image
Dependent Types have been on my radar for a while. I had a bit of a struggle wrapping my head around them in Haskell, so finding them in Lean was a welcome surprise. I'm only a couple of weeks in with Lean, but I'm already sold — it scratches the itch I didn't quite manage to scratch in Haskell. Coming from Haskell also helps; the language feels familiar enough that the learning curve isn't too steep. In this short write-up, I compare two Word Puzzle solver implementations: one in Haskell, one in Lean 4 (the latter being my very green attempt). Here's what I found. Overview of the Problem I built both projects to solve an identical problem: given a pool of 4–9 lowercase letters and a mandatory letter, filter a dictionary file for words that can be spelt from the pool. My Haskell version uses pull-based streaming I/O with the io-streams library and applicative validation via Data.Validation . For my Lean 4 attempt, I used dependent types with compile-time...

Tools for Functional Programming in Lean 4

Image
I've been busy this month learning about the success of LLMs in the Mathematical Olympiad . What interested me was not the result itself, but the tools used by the AI teams. They used the proof assistant called Lean . Lean is an interactive theorem prover and functional programming language. It also has dependent types. That opened up a rabbit hole that has consumed me for the past three weeks. So the yak shaving began… Neovim My editor of choice, Vim , did not support Lean . That meant retooling from Vim to Neovim . Instead of keeping my old Vim configuration, I decided to go fully Neovim-native with Lua configuration. That meant reviewing my Vim plugins and syntax files. The move was made a little harder because the version of Neovim available on Debian testing is v0.11.6. Many useful features landed in Neovim v0.12 and later, but those are not yet available on Debian testing. They are, however, available on Debian unstable . I just have to be patient. So, for each Vi...

How I Use Notebook LM for Research Deep Dives and Study Guides

Image
What is it? Notebook LM is a research and study companion that helps you work with your own source material. I have been using Notebook LM for nearly a year to help prepare blog posts and do deep dives into topics that interest me. My usual workflow is simple: I collect trusted sources as documents, PDFs or web links, upload them into a notebook, then use chat to interrogate the content. From there, I use studio features to generate podcasts, video overviews, infographics, and custom reports. In practical terms, Notebook LM feels like a custom ad hoc retrieval-augmented generation (RAG) tool. You upload your documents, then query it in context rather than relying on a general model response. Custom Personas The default experience keeps improving, with better templates, export options, and integration with tools such as Gemini and Google Drive. Those defaults are a good starting point, but I get better outcomes when I add custom personas. Custom personas let me control scope,...

The Evolutionary Origins of Mushrooms and Mycelium

Image
Over the weekend, I had the chance to explore a local forest with my partner. As we wandered along the track, we came upon a variety of mushrooms and fungi sprouting from the forest floor. It was a magical moment that sparked my curiosity about these fascinating organisms. When I think of the terrestrial world, I usually picture plants as the foundational pillars of life on land. However, long before the first leaves reached for the sun, a vast, hidden network was already laying the groundwork: fungi . What fascinates me about fungi is how they exist in a category entirely their own—neither plant nor animal, yet holding the world together. Molecular evidence suggests they diverged from a common eukaryotic ancestor roughly 1.5 billion years ago (much like the deep evolutionary history I explored in my post on LUCA ). Surprisingly, they are closer evolutionary cousins to animals than plants. In their earliest days, these organisms likely lived in water and possessed flagella . But a...

How to Encode Your Engineering IP into AI Agent Skills

Image
1. The Problem: AI Amnesia We’ve all been there. You’re working with an AI agent, and for a moment, it feels like magic. Then, five minutes later, it forgets the architectural decision you just made and defaults to some generic, shallow solution. It’s disconcerting. The truth is, AI-assisted development often lacks discipline. We’ve moved away from rigorous systems and into "vibe coding"—just hoping the right prompt will magically give us a maintainable codebase. It rarely does. Matt Pocock nailed the core frustration: You have access to a fleet of middling to good engineers that you can deploy at any time. But these engineers have a critical flaw: they have no memory. They don't remember things they've done before. I’ve learned that the only way to keep these agents on track is to stop treating them like magic chatboxes and start treating them like disciplined (if forgetful) engineers. The fix? Agent Skills. These are modular, encoded processes that force...

The Brainless Problem Solver: Why Nature's Solutions Matter

Image
Introduction: The Smartest Single Cell My interest in slime mould was piqued when I read Active Context Compression: Autonomous Memory Management in LLM Agents and learned that the design drew inspiration from Physarum polycephalum . In maze experiments, the mould prunes branches that do not lead to a reward and reinforces productive paths. That simple strategy maps surprisingly well to how we now think about managing context in large language model (LLM) systems. That connection led me to look more closely at the organism itself. Physarum polycephalum looks, at first glance, like a vibrant splash of yellow paint or a forgotten kitchen spill. Yet this "blob" is a syncytium: a single, massive cell containing billions of nuclei that share one continuous cytoplasm. It might be the world's most sophisticated "brainless" computer. What captivates me is its capacity for primitive cognition. Without a single neuron, it solves mazes, remembers past stimuli, and ...

Challenges on the Path to AGI

Image
Since 1956 one of the central goals of AI is achieving Artificial General Intelligence (AGI). Recently we have seen amazing advances in AI, but there are still important challenges to solve before we get there. In this article, I draw on the AAAI 2025 Presidential Panel report to outline what the AI community sees as the critical gaps that must be resolved before AGI can be achieved. AI is in a strange place right now. New benchmark results can make it seem as if the field is nearly solved. Yet these systems still fail basic common-sense tasks that humans manage with little effort. That gap is why true AGI still feels a long way off. In this article, AGI means an AI that can perform as well as a human across a wide variety of tasks, not just produce fluent text. The big problem is what researchers call the "Reasoning Paradox." Today's Large Language Models (LLMs) are very good at producing language that sounds like reasoning, but that is not the same as reliable for...