Massively Collaborative Research
bbchallenge logo
The Busy Beaver Challenge

Coq-BB5

Apr 2024 · mxdys

Information: the review system is currently extremely minimal. Any ideas for improvement are welcome.

Reviewers URL Notes
Yannick Forster, Théo Zimmermann https://discord.com/channels/960643023006490684/1218877181321678928/1247952831718359100 Reviewers agreed that the statement of [the formal theorem](https://github.com/ccz181078/Coq-BB5/blob/d5e7cb1fc332da3334215d857755ef355ccc6b9e/BB52Statement.v#L73) corresponds to "BB(5) = 47,176,870" and that the proof compiles without particular issues or concerns, only relying on standard axiom `functional_extensionality_dep`.