# quanglee · field notes > Interactive, long-form writing on AI systems, infrastructure and algorithms by quanglee, senior software engineer in Paris and math, tech and AI enthusiast. Every article is static HTML; interactive figures also carry a text description of what they show. ## Articles - [Mistral Large 4, seven months behind the frontier](https://quanglee.dev/blog/mistral-large-4/): Mistral Large 4 is the best model built outside the US and China and a big jump from Large 3. Independent tests put it about seven months behind the US labs and behind five Chinese open models, and a task on it costs about fifteen times more than on the small US models with the same score. (2026-10-12) - [🇦🇷🐐 Messi in numbers](https://quanglee.dev/blog/messi-in-numbers/): Lionel Messi made football look like art, and no spreadsheet can hold that. But the spreadsheet still says it, plainly. The best forward who ever played and the best playmaker who ever played are the same person. (2026-10-09) - [How Lean checks a proof](https://quanglee.dev/blog/how-lean-checks-a-proof/): Lean is a programming language in which a theorem is a type and a proof is a program, checked by a small kernel. This post covers how that works, where it can still go wrong, and why it lets language models write proofs nobody has to read. (2026-10-07) - [OpenAI's 722 math manuscripts](https://quanglee.dev/blog/openai-722-math-manuscripts/): On 6 October OpenAI published 722 machine-written math papers with claims on the Unique Games Conjecture, the colouring of the plane, a $5,000 Erdős problem and dozens of other open problems. This post goes through the claims, the parts that come with Lean proofs, and the first day of reactions. (2026-10-07) - [DeepSeek V4.1 vs GLM-5.3, and how far both are from Claude Code and Codex](https://quanglee.dev/blog/deepseek-v4-1-vs-glm-5-3/): DeepSeek V4.1 and GLM-5.3 compared on agentic work and coding in two weight classes, next to the closed models behind Claude Code and Codex, with benchmark scores by task type, speed, cost per solved task and reports from daily use. (2026-10-06) - [How a transformer reads](https://quanglee.dev/blog/how-a-transformer-reads/): A walk through the parts of a transformer, from tokens to sampling, with a working figure for each step. (2026-10-03) - [LeetCode 1977: number of ways to separate numbers](https://quanglee.dev/blog/leetcode-1977-separate-numbers/): A hard DP that's worth knowing, because it stacks three classics in one problem. Partition DP, prefix sums and an LCP table take it from O(n³) to O(n²). (2026-06-22) - [Behind prompt caching: a friendly intro to KV caching](https://quanglee.dev/blog/kv-caching-explained/): What actually happens when a provider says your prompt is cached. The trick underneath is called KV caching, and it's a small idea with a big memory bill. (2026-04-30) - [The real cost of running agentic AI, and how not to go broke](https://quanglee.dev/blog/agentic-ai-cost/): Agents loop, and every loop resends everything. Where the tokens actually go, how prefix caching claws most of it back, which benchmarks matter when you pick a model, and a router you write yourself. (2026-04-28) - [Elasticsearch best practices, and a few twists nobody mentions](https://quanglee.dev/blog/elasticsearch-best-practices/): What I check first when an Elasticsearch cluster gets slow. Shards, segments, refreshes, and the profiling result that changed how we fetch ids. (2025-07-15) - [Notes on making this site](https://quanglee.dev/blog/notes-on-making-this-site/): The site, twice. A one-font page I shipped in april, then a rebuild with figures you can poke, a small green critter and a status bar. (2025-04-27) ## Elsewhere - [GitHub](https://github.com/winlp4ever) - [dim0](https://dim0.net): a thinking canvas - [minmux](https://minmux.dev): a terminal for agentic coding - [kiframe](https://github.com/vcmf/kiframe): scenario to product demo video (in development)