If you have feedback for me, you can fill out the form at https://w-r.me/feedback .
Or you can email me, at [the second letter of the alphabet]@[my username].net
I do not get any notifications about replies to my comments or posts. I may take a long time to respond to them, or never respond.
fyi for those of you who do math: Some coding agents are now (~barely) able to usefully write Lean proofs, for not-totally-trivial statements.
This matters to me (and might matter to you) due to differences in how easy it is to understand Lean statements + have the Lean compiler check the proofs, compared to correctly hand-verifying proofs in English.
I spent a couple hours this weekend having them prove a thing about graph theory that’s useful for some distributed systems stuff I was thinking about last year. Before going through the process I was only ~80% sure the statement was true; I’m now more like 99%; that last 1% would mostly come from my more-carefully double checking that the Lean statement corresponds to the thing I actually care about.
For this problem at least, Claude was superior to Gemini at actually using the lean compiler and iterating, but Gemini was superior at structuring the code at the top level / figuring out the broad strokes of the proof.
Very highly recommend using agents instead of trying to do this via chat, since the process here clearly required a feedback loop rather than merely spitting out correct proofs.