This repo is an exploratory dive into the Lean theorem prover, using it to verify the proof of the Byzantine Generals Problem. Alongside the verification in src/final.lean
, a paper is presented outlining the problem, it's proof, and the learnings I took away from trying to verify this complicated result in Lean.
mpekala23 / formalbyzantine Goto Github PK
View Code? Open in Web Editor NEWA formal proof of the Byzantine General's problem in the Lean theorem prover