A very cool and simple introduction into Lean and what makes it interesting. I’m not sure exactly what draws people in this direction but it’s cool to see the progress that’s being made here.

Solvers are very annoying to setup and plug your problem into if you’re using them regularly. That’s why hooking them into LLMs to do the annoying manipulation work is an amazing idea.

It’s always been my feeling that TLS has unacceptable collateral damage in how it breaks the web for normal people. That’s considered a bit of a crank opinion, but I’m definitely not the only person who feels that way.