On January 7, Terence Tao posted about an Erdős problem being solved "more or less autonomously by AI." The key was Lean - a formal proof language that can mechanically verify mathematical arguments. Tao observed: "The combination of reasonably competent AI text generation and modification capabilities, paired with the ability of formal proof assistants to verify the informal arguments thus generated, allows for a much more dynamic and high-multiplicity conception of what a writeup of an argument...

Your browser does not support the video tag. I built a research project this weekend at the intersection of chess and frontier models. Not to play chess - agents and LLMs are getting eerily competent at that - but to explore whether they can help you understand openings, themes, attacking plans, and positional concepts through an interactive coaching interface. The core idea: build an agent harness with access to all the tools a chess player uses when studying. Stockfish [2] for deep analysis. The Masters...

Andrej Karpathy posted an incredible 2025 LLM Year in Review. It is a totally salient take (obviously, he's brilliant!) and mirrors a lot of my experiences in the trenches. I have a slightly different take on a point or two below. ⪼ Like Karpathy, I believe there is a ton of value for the application layer above LLMs. I think the model providers are making a generally useful brain, but its frozen in a moment and for now at least, we need prompt and context engineering, specialized tools, and verification for...

There are people in the industry and perhaps in your organization that have a lot of context. They have good judgment, they have reasonable design sense, they know a lot about your product, the market fit, the ideal customer profile. They understand the competitive landscape - who the different players are, what they're doing, where the opportunities lie. And on top of all that, they may also be high-end software developers. Recently, I was watching an interview with Terence Tao [1], who's an Australian-American...

I want to talk about a genuinely surprising personal engineering breakthrough I've experienced. Over the past 3 days, I challenged myself to experiment with a true AI-native development workflow based on the advancements I've observed over the last few months. I chose Cursor Ultra, Warp, superwhisper, Claude 4 Opus and a few other capable models for different purposes, and focused on creating the most comfortable and fluid experience possible. I'll provide my background so you can decide if this is relevant to...