I know you all have better things to do with your life but ... As I've mentioned too many times I'm trying to merge LEAN proof technology with computer algebra (the SANE project in Axiom). That involves proving algorithms.
LEAN currently seems more focused on straight math rather than mathematical algorithms but I'm hoping that will change if we can find a way toward proving computer algebra programs. This has already been done with Buchberger's Groebner Basis algorithm in Coq, for example, which was implemented in Axiom years ago. One key question is how to abstract software implementations into a mathematically tractable form suitable for processing by LEAN. The "crossover" bridge between software algorithms and LEAN seems to be best captured by Leslie Lamport's TLA+ approach https://www.youtube.com/watch?v=p54W-XOIEF8&list=PLWAv2Etpa7AOAwkreYImYt0gIpOdWQevD&index=2 This rather brief course gives all the needed ideas. Lamport provides a way to reduce computer algorithms into mathematical expressions. It seems to me we are one PhD student away from combining that approach with LEAN to provide a fairly comprehensive proof assistant capable of handling algorithmic proofs. The TLA+ machinery combined with the LEAN machinery seems to me to be a path to including algorithmic proofs in LEAN. If any of you have a grad student looking for a PhD thesis topic this might be a useful suggestion. I'm no longer associated with any University so nothing I do will likely see the light of day. Tim
