News for hackers. Stuff that matters.
Re:What mathematicians should know about the Lean Theorem Pr... by laichzeit0 on Saturday October 10, 2026 @02:20AM (#50030197)
> Coq (renamed Rocq last year)

This is lamentable.

Re:What mathematicians should know about the Lean Theorem Pr... by jjgreen on Saturday October 10, 2026 @07:22AM (#50031802)
If they must fold to American prudery, at least Dinde ...
Re:What mathematicians should know about the Lean Theorem Pr... by dfdydx on Saturday October 10, 2026 @08:39AM (#50032352)
Still waiting for the outrage on "bits".
Re:What mathematicians should know about the Lean Theorem Pr... by 123a7a on Saturday October 10, 2026 @09:24AM (#50032715)
Indeed. The people who suggested the change in 2021 and the mailing list threads have been purged from the search engines, but this thread is still here:

https://news.ycombinator.com/item?id=26738980

Talia Ringer, the main proponent, now writes posts that AI will turn out OK (and works on proof automation for programs so that more software engineers can become unemployed):

https://terrytao.wordpress.com/2026/09/17/becoming-a-benchma...

Remember that when you live under a bridge after having been fired that the world is fine because the great social injustice of the "Coq" name has been eradicated!

Re:What mathematicians should know about the Lean Theorem Pr... by bumbledraven on Saturday October 10, 2026 @07:41PM (#50038249)
Did anyone consider keeping the current name but changing the pronunciation to “coke”?