Notes: 19th June 2026
Not much to say this week really, just that I went to a workshop in Bonn on Mathematics, Formalisation and AI while continuing to fiddle about with the new Idris core and evaluator.
The workshop was interesting in lots of ways, with lots of exciting possibilities discussed. Though it was also (to be kind) a bit annoying in others, mostly because I didn't feel there was enough acknowledgement of the ethical and environmental implications or the impact on education, or, really, much about the negatives at all. Still, I learned how Mathematicians are using LLMs to translate proofs into Lean, and it's really cool that it works at all and I'm sure we can learn a lot from them. I gave a talk about Idris (just a general introduction) and talked about places where I felt LLMs might have some value, and how I believe that a well defined checkable core is essential if we're going to trust these things, while also expressing some scepticism and general concern about the ethical and environmental implications.
I have lots to say on this topic, but I think I'll save it for when I see people in 3D and not for a ramble on the internet. Except to say that several participants seemed to believe that LLMs are exciting because they're going to keep getting better for ever. I'll just leave that there.