rocq-prover/rocq on Hacker News

Some argue that Lean breaks a few type-theoretical properties. See full discussion here: https://github.com/rocq-prover/rocq/issues/10871

comment by xvilka · 2026-09-05 · in Formalizing Fermat's Last Theorem

…Not sure if it might hinder the automation with the AI. [1] https://artagnon.com/logic/leancoq [2] https://github.com/rocq-prover/rocq/issues/10871

comment by xvilka · 2026-02-21 · in Lean 4: How the theorem prover works and why it's the new competitive edge in AI

…[2] https://lawrencecpaulson.github.io/2023/08/23/Propositions_a... [3] https://github.com/rocq-prover/rocq/wiki/The-Logic-of-Coq#wh... [4] https://rocq-prover.org/doc/V8.15.0/refman/addendum/sprop.ht... [5] https://ncatlab.org/nl

comment by 4ad · 2025-07-02 · in Types of Types: Common to Exotic

There are, you can check this discussion [1] as well. [1] https://github.com/coq/coq/issues/10871

comment by xvilka · 2024-04-24 · in New Foundations is consistent – a difficult mathematical proof proved using Lean

The page summarizing the considered new names and their pros/cons is interesting: https://github.com/coq/coq/wiki/Alternative-names Naming is hard...

comment by yaantc · 2023-12-27 · in Change of Name: Coq –> The Rocq Prover

…software French names. [1] https://fr.wiktionary.org/w/index.php?title=coq&oldid=325194... [2] https://github.com/coq/coq/wiki/Alternative-names

comment by nequo · 2023-09-22 · in Lean, Coq and other proof assistants: Visualising proofs as trees

…was very famously struck down by Gödel. But we've definitely gotten it right this time... [0] https://github.com/coq/coq/issues/4294

comment by wk_end · 2023-08-31 · in Mathematical proof is a social compact

…less offensive? There were a number of excellent proposals [2] that seemed to die on the vine. [1] https://github.com/coq/coq/wiki/Alternative-names [2] https://github.com/coq/coq/wiki/Alternative-names#c%E1%B5%A3...

comment by harveywi · 2023-06-22 · in Functional Programming in Coq

…- Coq critical bugs (some of these mention potential ways to prove false): https://github.com/coq/coq/blob/master/dev/doc/critical-bugs (You can also get the theorem prover itself to hang or crash; if you work with theorem provers of

comment by armchairhacker · 2023-06-06 · in Counterexamples in Type Systems: programs that crash, segfault or explode (2021)

Which category does Coq go in? https://github.com/coq/coq With code example: https://github.com/coq-community/coq-100-theorems/blob/maste...

comment by sebstefan · 2023-05-04 · in The seven programming ur-languages (2021)

…https://github.com/moby/hyperkit/tree/v0.20210107 And while niche, Coq is not exactly unheard of: https://github.com/coq/coq/tree/V8.16.1 If you weren't already aware, GitHub supports searching by the repo's more prominent language:…

comment by mdaniel · 2022-12-17 · in Ask HN: What Is OCaml Used For?

here are a few - https://github.com/coq/coq - https://github.com/mirage/mirage - https://github.com/returntocorp/semgrep - https://github.com/bcpierce00/unison See https://v2.ocaml.org/learn/companies.html for some more leads, as lots of…

comment by abathologist · 2022-12-16 · in OCaml 5.0 Multicore is out

Thanks I guess Martin-Löf speaks about W-Types. An implementation and examples in Coq: https://github.com/coq/coq/wiki/WTypeInsteadOfInductiveTypes Still waiting for the year of W-Types

comment by hackandthink · 2022-10-02 · in Great Works in Programming Languages (2004)

…scholarship. Still, the community has been quietly mulling a name change for a while [1]. [1] https://github.com/coq/coq/wiki/Alternative-names

comment by 0xcde4c3db · 2022-01-15 · in Woob: Web Outside of Browsers

…[3] (Lean) https://www.ma.imperial.ac.uk/~buzzard/xena/natural_number_g... [4] https://github.com/coq/coq/wiki/The-Logic-of-Coq

comment by siraben · 2021-07-30 · in The Fundamental Theorem of Algebra in ACL2

…might fix more issues for Coq. Will they follow the Arend[2] path? That remains to be seen. [1] https://github.com/coq/coq/pull/10764 [2] https://arend-lang.github.io/about/arend-features

comment by xvilka · 2021-06-20 · in Mathematicians welcome computer-assisted proof in ‘grand unification’ theory

…the discussion[1] if the Coq is suitable for number theory as quotients are ubiquitous here. [1] https://github.com/coq/coq/issues/10871

comment by xvilka · 2021-06-19 · in Mathematicians welcome computer-assisted proof in ‘grand unification’ theory

…the name, but hope we can keep the French origin. "LPC" for "Le Prouveur Coq" is a good idea https://github.com/coq/coq/wiki/Alternative-names .

comment by Zababa · 2021-06-15 · in Coq mulls new name for programming language

From their wiki page ( https://github.com/coq/coq/wiki/Alternative-names ): > Reason for discarding: Con is French slang for vulva. This will inevitably lead to categorical jokes about co-con aka... the problem we started with. > Reason…

comment by Fiahil · 2021-06-15 · in Coq mulls new name for programming language

…those fond of playing with words, oh geez, these lines of high quality Côq made me so happy. [1] https://github.com/coq/coq/wiki/Alternative-names

comment by samizdis · 2021-06-15 · in Coq mulls new name for programming language

…list) Here are some other links related to the discussion: * wiki, where anyone can add proposals: https://github.com/coq/coq/wiki/Alternative-names * chat: https://coq.zulipchat.com/#narrow/stream/237655-Miscellaneou... * forum:…

comment by clarus · 2021-04-08 · in Renaming Coq

Yes, it did shut down. Other links related to it: * wiki, where anyone can add proposals: https://github.com/coq/coq/wiki/Alternative-names * chat: https://coq.zulipchat.com/#narrow/stream/237655-Miscellaneou... * forum:…

comment by clarus · 2021-04-08 · in Renaming Coq

From https://github.com/coq/coq/wiki/Alternative-names > others getting harassed when they said they were working on Coq It's hard for me to imagine anyone getting harassed over this, who are these people who haven't moved past puberty but…

comment by capableweb · 2021-04-08 · in Renaming Coq

The proposals: https://github.com/coq/coq/wiki/Alternative-names I particularly like Chapon, if the name was to change (from the announcement: this is not yet a commitment toward a renaming )

comment by hadrien01 · 2021-04-08 · in Renaming Coq

They do, it's linked from the page: https://github.com/coq/coq/wiki/Alternative-names

comment by throwaway287391 · 2021-04-08 · in Renaming Coq

haha they can't get away from it https://github.com/coq/coq/wiki/Alternative-names#gaul

comment by abledon · 2021-04-08 · in Renaming Coq

…work with. There's some info here about how Lean does realizability with pervasive use of choice: https://github.com/coq/coq/issues/10871#issuecomment-5466412...

comment by lakecresva · 2020-11-21 · in Why is dependent type theory more suitable than set theory for proof assistants?

…on their GitHub[6]. [1] http://coq.inria.fr/ [2] https://learnxinyminutes.com/docs/coq/ [3] https://github.com/coq/coq [4] https://softwarefoundations.cis.upenn.edu/ [5] https://coq.discourse.group/ [6]…

comment by xvilka · 2020-04-06 · in Doing a math assignment with the Lean theorem prover

Coq 8.11.0 was recently released: https://github.com/coq/coq/releases/tag/V8.11.0 This version introduces a new tactic language, Ltac2.

comment by TheAsprngHacker · 2020-02-01 · in Coq: A program specification and mathematical higher-level language

…of quotients also breaks normalization, but they don’t care as much about that as Coq devs do. [0]: https://github.com/coq/coq/pull/10390#issuecomment-554316311

comment by jmgrosen · 2020-01-28 · in Coq is a Lean Typechecker

https://github.com/coq/coq/wiki/Presentation >Did you really need to name it like that? >Some French computer scientists have a tradition of naming their software as animal species: Caml, Elan, Foc or Phox are examples of this tacit…

comment by sincerely · 2019-11-26 · in Learn Coq in Y Minutes

…[3] https://arxiv.org/abs/1907.07794 [4] https://github.com/UCSD-PL/proverbot9001 [5] https://github.com/coq/coq/issues/10871

comment by xvilka · 2019-10-31 · in Can Computers Prove Theorems?

…just asked[1] Coq developers straightly. I recommend to read their discussion and explanations. [1] https://github.com/coq/coq/issues/10871

comment by xvilka · 2019-10-26 · in Metamath Zero, a bootstrapping theorem prover

I strongly recommend reading https://github.com/coq/coq/issues/10871#issuecomment-5404526... which was written a few hours ago broadly in the vein of Lean vs. Coq, more precisely on the issue of how Lean handles quotients.

comment by ocfnash · 2019-10-10 · in The Future of Mathematics? [video]

…Foundations[2]. Probably these can be used as a more substantial "base" for this machine. [1] https://github.com/coq/coq [2] https://github.com/UniMath

comment by xvilka · 2019-07-04 · in The Ramanujan Machine: Using algorithms to discover new mathematics

…and there doesn't seem to be any way to abstract over the raw `cofix` form) and in theory ( https://github.com/coq/coq/issues/5288 https://github.com/coq/coq/issues/6768 ). Agda's co-patterns are nicer to work with, but still require weird…

comment by chriswarbo · 2019-03-06 · in Lambda Cube

…strongly-worded disclaimer. Just importing it would probably fix the described memory issue. *) https://github.com/coq/coq/blob/307f08d2ad2aca5d48441394342a...

comment by MichaelBurge · 2017-08-26 · in Writing a formally-verified image browser in Coq and Haskell

…(which also has a bunch of interesting subprojects, like irmin) https://github.com/mirage * coq https://github.com/coq/coq * flow https://github.com/facebook/flow * CompCert https://github.com/AbsInt/CompCert * frama-c…

comment by ernst_klim · 2017-07-16 · in A deep dive into Multicore OCaml garbage collector

…- Adds static typing to JavaScript to improve developer productivity and code quality. https://github.com/coq/coq - Coq is a formal proof management system. It provides a formal language to write mathematical definitions, executable…

comment by 0xmohit · 2016-08-02 · in Show HN: Learn Functional Programming Using Haskell

…compared to the work required to actually get this done. Here's that development in Coq right now: https://github.com/coq/coq/tree/trunk/theories/QArith Does HoTT really make these things simpler to write and prove? If so, what is the…

comment by jbapple · 2014-09-07 · in A new foundation for mathematics