This week's been a busy news week with more human endeavour having their AI reckonings. Mathematics had its turn with Navier–Stokes, which got me thinking about formative assessment in the CST Tripos. Meanwhile I spent a ton of my time triaging endless security bugs found by LLMs in open source code, but the humans aren't dead yet and there's no need to panic. I also had a lovely visit from Echo Labs, and went back to fighting Windows in Eio and GeoTessera.
1 Every field is getting its own AI reckoning
Everyone was panicking about cybersecurity a few months ago being turned on its head by AI, and this week it was the turn of the mathematics community. Tristan Buckmaster and Levent Alpöge were hacking on a solution to the Navier–Stokes problem for about a year. OpenAI heard a rumour of a breakthrough, pointed their giant cluster at it, and had a solution a few days later. There's obviously been a lot of controversy around this shameless race to publicity, and Simon Willison drew a parallel with my observation in cybersecurity that a mere rumour of a bug is enough to find an exploit these days, as did Bruce Schneier. The fundamental premises of whole fields of endeavour are shifting beneath our feet in real time...
Jon Sterling has written a great piece on the maths fallout, having co-signed the Fields Medalists' declaration that the goals of the AI companies and the mathematical community are "severely misaligned". He notes that (academic) mathematics is unprepared for the ruthless scooping culture of an industry with trillions on the hook.
Daniel Litt wrote more positively about a beginning for mathematics, where he argues that since the production of mathematical text is now disconnected from understanding it, the profession should reward understanding directly. PhDs should be awarded mainly on a rigorous (in person) defence, graduate admissions by interviews, and promote an interactive seminar culture in which speakers explain their topic (a bit like WG2.8 rules where the speaker must get the audience to ask questions for half the time). He expects that we will need more human mathematicians, not fewer, if we shift culture like this.
1.1 Formative before summative assessment in the Tripos
Daniel's essay got me thinking about how we do assessments in the University. I share many of Jon Sterling's concerns about how we can help the next generation of scholars "survive and thrive" and navigate this ever shifting landscape. Simon Peyton Jones pointed out to me over our morning coffee that the difference between formative and summative assessment matters a lot here to set incentives right for students. Formative assessment gives feedback during the students' learning process, whereas summative assessment grades what they have learnt at the end. This 2022 paper finds that the formative option "was more effective on academic motivation, test anxiety, and self-regulation skill." We're really lucky in Cambridge that we have a lot of human student contact time due to the supervision system, and hence less pressure to resort to LLMs in teaching.
In fact, the rule of thumb needs to be that AI use should never be permitted if it's for the purpose of passing formative assessments. It's a complete waste of time for everyone involved to show up to a supervision having faked out the questions posed. They weren't set because the supervisor cares about the answer, but because they want to know how well the student is progressing in order to give them tailored advice for the next hour! I generally want the early years of our Computer Science Tripos to focus more on formative work that sparks the joy of computer science, rather than crushing students' spirits early with pressure-filled exams.
One other reason to have useful formative assessments is that it reduces the chances of crashing and burning on our end-of-year exams, which are still written on pen-and-paper. I'm hoping that improvements like interactive lecture notes will encourage experimentation among new students, as will expanded supervision material with hard, challenging problem sets for students who want to push themselves. For students searching for projects in the short term, I've also refreshed my Part II and MPhil project ideas this week! Please do get in touch if one catches your interest, ideally after researching it a little first. On my reading list is also Kathi Fisler et al's note on Teaching Novice Computing and Programming in the Agentic AI Era.
2 Don't panic, the humans aren't dead yet
I was forced to spend most of the week triaging hundreds of credible bugs that Scrutineer has turned up, and will open fixes next week. The first to be published was a set of cstruct indexing bugs, immortalised in OSEC-2026-20. Others in the OCaml community are in the same position, with Sadiq Jaffer commented to me that he's fielding a big batch of reports in the runtime (I helped him out by supplying him with a few more from Scrutineer).
This is a rather depressing way to do open source though, and in the long term it's a losing proposition if all the cards are stacked on the attackers' side. So as a side project I've been experimenting with Lean and Rocq to build defences that can give open source maintainers an edge by having better specifications, along the same lines as work I did on POSIX specifications in 2013. I'll write more as it matures next week, but it follows on from my project ideas on Lean enforcement automata and an antibotty testbed.
The stakes get even higher when we add physical interconnects into the mix. This week, we put up the NERVE preprint led by Zahra Tarkhani that shows how brain-computer interfaces can be forged, replayed and backdoored. The attacks hijacked all three CYBATHLON BCI tasks in about eight seconds, including one where a misclassification of the user 'thinking' input tips over a robotic arm.
However, while all these issues look bad, none of it justifies the ludicrous panic espoused this week. There may be a short term window where we have a surge of such issues, but defences can and will catch up. In The contagion of fear, Bryan Cantrill argues that domain experts hold the public's trust and must be most circumspect precisely when raising the alarm. I completely agree: AI brings huge opportunities and serious downsides, and big changes are happening, but our role as computer scientists is to stay grounded and realistic rather than shout "fire" in a crowded theatre.
3 Echo Labs visits
I was delighted to spend a morning with Mike Harfoot and Ștefan Istrate, who have both recently joined the stellar team at Echo Labs to work on ecological foundation models. David Coomes and I went over the latest developments in Tessera, including the habitat maps that Michael Dales and Aneesh Naik are leading development of.
In turn, Mike and Ștefan filled me in on some of the ecosystem datasets they're assembling, including bioacoustic data. There are some fascinating possibilities developing in terms of multimodal GeoFM, but also in terms of quick wins for increasing the accuracy of counterfactual reasoning for interventions. I'm looking forward to working on this more with Team Echo as we progress to a global product!
4 Getting back to fighting Windows
My Windows frustration continued this week. My fixes in Eio for NT path handling and rename were merged, and rename was harder than expected because Windows treats overwriting files and directories differently. Anonymous pipes and process spawning are now open for review, but I think I still need to port the pipe implementation to IOCP as there's no working combination using Unix.select that I can find. This will hopefully get Forester working end-to-end on Windows though, and hopefully help Patrick Ferris with his new shell!
I also took advantage of a working Windows machine to release GeoTessera 0.10.3, which improves Windows support for Zarr. I also removed ppx_cstruct's dependency on ocaml-migrate-parsetree so that it all works on recent OCamls, and released json-pointer for RFC 6901 pointer manipulation from OCaml.
5 Tip of the week: unlocking the macOS keychain over SSH
I SSH'd into my Mac this week and found that git push failed, even though it worked fine at the keyboard earlier. Git on macOS stores credentials such as my Overleaf git tokens in the login keychain via the osxkeychain credential helper. The remote fix is to simply run security unlock-keychain first, which prompts for your login password and then makes the stored tokens available for the rest of the session.