Posts

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 Vim plu...

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...

Managing my Debian Systems with Ansible

Image
Years ago, as a DevOps engineer, I managed systems using various automation tools. However, for managing my own workstations, I chose Ansible and found a streamlined way to keep my Debian systems consistent without turning the whole exercise into another full-time job. What I like most about Ansible in this context is that it gives me structure without much friction. I can keep a clear separation between work and home machines; I can decide exactly which roles belong on which hosts through the inventory ; and I get useful safeguards such as ansible-lint and dry runs before I touch a live system. I also find the tooling approachable. The command line is simple, the module ecosystem is broad, and the documentation is good enough that I rarely feel like I am fighting the tool. The project itself is organised around small, isolated roles. Each role lives in its own directory under roles/ , with its own tasks, files, and variables, so a change to something like vim does not leak i...