Frankly speaking ...

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

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