Skip to content

feat(FLP): define pseudo-consensus and prove that it is implied by consensus - #718

Merged
fmontesi merged 6 commits into
leanprover:mainfrom
ctchou:flp-pseudo
Jul 29, 2026
Merged

feat(FLP): define pseudo-consensus and prove that it is implied by consensus#718
fmontesi merged 6 commits into
leanprover:mainfrom
ctchou:flp-pseudo

Conversation

@ctchou

@ctchou ctchou commented Jul 13, 2026

Copy link
Copy Markdown
Collaborator

This PR defines the notion of a fault-tolerant "pseudo-consensus" algorithm, which is central to Völzer's proof, and proves that every f-tolerant consensus algorithm is also a f-tolerant pseudo-consensus algorithm. This resilt is intuitively obvious and is stated without proof in Völzer's paper, but it turns out to require quite a bit of formal machinery (given in FairSchedular.ean) to prove.

Zulip discussion: #CSLib > Impossibility of distributed consensus

@fmontesi fmontesi left a comment

Copy link
Copy Markdown
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I've just found a typo, rest looks good and can be queued once fixed.

Comment thread Cslib/Computability/Distributed/FLP/PseudoConsensus.lean Outdated
@fmontesi
fmontesi enabled auto-merge July 29, 2026 16:16
@fmontesi
fmontesi added this pull request to the merge queue Jul 29, 2026
Merged via the queue into leanprover:main with commit a1faa28 Jul 29, 2026
2 checks passed
@ctchou
ctchou deleted the flp-pseudo branch July 29, 2026 16:34
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

2 participants