Reasoning about Algorithms

Stream: Is there code for X?

[Rian Neogi]

Hello everyone, I'm new to Lean. I was wondering whether were are any cases where reasoning about algorithms can be done in lean? This would include: Defining an algorithm in lean, proving its correctness in lean, analyzing its run time in lean etc.

More specifically, can one prove in lean that say the Miller-Rabin primality test correctly tests whether a number is prime with high probability and does so in polynomial time?

[Yuyang Zhao]

I think this is related to the formalization of complexity theory, but the it is still a difficult problem. Of course for specific problems, general complexity theory can be avoided.

[Anne Baanen]

Lean was originally created for formalizing algorithms so this is very much possible! A relevant example in mathlib is docs#lucas_lehmer.run_test, which implements the Lucas-Lehmer test.

[Anne Baanen]

I would recommend the Hitchhiker's Guide to Logical Verification for an introduction on verifying software using Lean (nb: I'm a co-author of the Guide)

[Jason Rute]

I’m not sure it is natural to verify run-time of Lean algorithms. Because of function extensionality, any two functions which give the same output are equal.

[Bolton Bailey]

Me and an undergrad mentee of mine worked on a formalization of the correctness and soundness of Miller-Rabin in Lean, unfortunately I never finished it to the point where it could be reviewed as a PR. You can see the branch here