clarus/falso
View on GitHub ↗ ★ 105 Coq
A proof of false in Coq.
7 mentions on Hacker News by 7 people: 1 story, 6 comments · first 2015-03-24 · latest 2024-09-26
20082026
-
…from some bug that allowed `false` to be proved [1]. It's just that hard---not really feasible. [1] https://github.com/clarus/falso
comment by lifthrasiir · 2024-09-26 · in Rewriting Rust -
…otherwise, then how can you reconcile the existence of falso (a coq verified proof of "false")? https://github.com/clarus/falso Proof and belief I think are pretty strongly intertwined, but I'm not going to pretend to have a particularly…
comment by TheNewAndy · 2024-06-20 · in Show HN: I made a puzzle game that gently introduces my favorite math mysteries -
…- Breaking Badfny: https://www.reddit.com/r/Coq/comments/x4d31y/breaking_badfny... - Falso (Coq): https://github.com/clarus/falso - Coq critical bugs (some of these mention potential ways to prove false):…
comment by armchairhacker · 2023-06-06 · in Counterexamples in Type Systems: programs that crash, segfault or explode (2021) -
…) who pointed out a flaw (now fixed) in Coq that allowed false theorems to be proved. Github link: https://github.com/clarus/falso
comment by archgoon · 2018-10-06 · in Formalizing 100 theorems in Coq -
Even coq have had its bugs where it was possible to prove that true is false: https://github.com/clarus/falso
comment by 0x0 · 2015-06-06 · in Verified Correctness and Security of OpenSSL HMAC -
Is the Coq bug you're thinking of this one, from earlier this year? https://github.com/clarus/falso
comment by schoen · 2015-06-01 · in Developing Provably-Correct Software Using Formal Methods