The past two months, I helped coordinate the "Phase Transitions..." research semester programme at CWI (https://www.cwi.nl/en/events/research-semester-programmes/phasecap-phase-transitions-in-combinatorics-algorithms-probability/). It ended last Friday, and still I feel "hungover" from the intensive blur of activities/developments/ideas. Very grateful to my team --Feri, Jop, Serte, Carla, Noela, Guus-- we did it!

In parallel, during the same two months, after the dawn of recognition of what has arrived (after a tip from Jeroen), I underwent a kind of phase transition myself. Avowed refusenik in March (see https://mathstodon.xyz/@kangmeister/115252549665766971); an "anti-Gemini" research working group in April; compulsive button-pressing in May. (And yes, I *know* it is easy to set it up for pressing fewer buttons...)

That poetic part of me (or whatever remains of it) is allured by the term, "cognitive surrender", if only to help in my search for the right words to describe the sharp changes underway in various facets of mathematical life/growth.

#CWI #combinatorics #algorithms #probability #conferences #generativeAI #formalization #lean #scientificpublishing

I'm trying out Aristotle and Lean Copilot for formalizing and proving theorems, and, so far, Aristotle feels way more powerful. Lean Copilot's suggestions aren't always right. Aristotle, on the other hand, can bring in previous lemmas, figure out missing hypotheses, and so on –besides, of course, finishing the proofs themselves.

Disclaimer: this is probably mostly down to the underlying model: Aristotle uses a specialized in-house model (within an agentic architecture), while Lean Copilot is using a more general-purpose one (and not a particularly strong one, at least in my setup... DeepSeek-R1, I think).

#lean #theoremproving #aristotle