Seong-Heon Jung (정성헌)Another cool Lean exercise: a verified implementation of the Boyer-Moore majority voting algorithm.
It's an O(n) time O(1) space majority element detection algorithm.
The 1981 verification of took the authors 20 hours. In contrast, I spent no more than 4 hours (including building the CLI tool) thanks to proof automation techniques like grind and omega.
