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`. |