Groups | Search | Server Info | Keyboard shortcuts | Login | Register [http] [https] [nntp] [nntps]
| From | Mild Shock <janburse@fastmail.fm> |
|---|---|
| Newsgroups | sci.logic |
| Subject | Having 2544 issues is probably a bad sign (Was: Maybe AGI should take over proving) |
| Date | 2025-07-15 18:34 +0200 |
| Message-ID | <1055vv3$2940k$1@solani.org> (permalink) |
| References | <104oa2l$r4na$2@dont-email.me> <104obqh$r4na$3@dont-email.me> <1055voq$293rt$1@solani.org> |
Hi, Having 2544 issues is probably a bad sign. I find this many issues here: https://github.com/rocq-prover/rocq/issues Mostlikely 90% of the issues can be move to the new discussion feature of GitHub. LoL Bye P.S.: Same holds for Scryer Prolog with 406 issues. Mild Shock schrieb: > Hi, > > Maybe AGI should take over proving. > Just take the humans out of the loop > of any programming, it leads to nowhere. > > Bye > > Julio Di Egidio schrieb: >> On 10/07/2025 14:01, Julio Di Egidio wrote: >>> The end of the world is nigh: >>> >>> <https://rocq-prover.zulipchat.com/#narrow/channel/237656-Rocq-devs-.26-plugin-devs/topic/status.20and.20future.20of.20the.20phase.20split/near/528029103> >>> >>> >>> From interactive proof assistant to completely upside-down and >>> completely broken, and not just on that at that point of course. >>> >>> And the fucking shamelessness... >> >> But we must thank MS for the nail in that coffin, too: they can't >> be satisfied with just a Lean broken by design, they must own the >> whole compartment: only poisoned meatballs for the public... >> >> -Julio >> >
Back to sci.logic | Previous | Next — Previous in thread | Next in thread | Find similar | Unroll thread
Coq/Rocq and how to completely break it Julio Di Egidio <julio@diegidio.name> - 2025-07-10 14:01 +0200
Re: Coq/Rocq and how to completely break it Julio Di Egidio <julio@diegidio.name> - 2025-07-10 14:31 +0200
Maybe AGI should take over proving (Was: Coq/Rocq and how to completely break it) Mild Shock <janburse@fastmail.fm> - 2025-07-15 18:31 +0200
Having 2544 issues is probably a bad sign (Was: Maybe AGI should take over proving) Mild Shock <janburse@fastmail.fm> - 2025-07-15 18:34 +0200
The Signal Collapse gives us System Uncertainty (Was: Having 2544 issues is probably a bad sign) Mild Shock <janburse@fastmail.fm> - 2025-07-15 19:01 +0200
Re: Coq/Rocq and how to completely break it Julio Di Egidio <julio@diegidio.name> - 2025-11-30 09:52 +0100
Re: Coq/Rocq and how to completely break it Julio Di Egidio <julio@diegidio.name> - 2025-11-30 10:00 +0100
SWI Agent Provocateur gets kicked out of Rocq? (Re: Coq/Rocq and how to completely break it) Mild Shock <janburse@fastmail.fm> - 2025-11-30 10:28 +0100
How to get GigaLIPS for Transitive Closure (Was: SWI Agent Provocateur gets kicked out of Rocq?) Mild Shock <janburse@fastmail.fm> - 2025-11-30 11:20 +0100
I am already using this method for 20 years [AI Effloreszenz] (Was: How to get GigaLIPS for Transitive Closure) Mild Shock <janburse@fastmail.fm> - 2025-11-30 11:32 +0100
New branding Accelerated Linear Algebra [OpenXLA C++] (Was: I am already using this method for 20 years) Mild Shock <janburse@fastmail.fm> - 2025-11-30 11:43 +0100
When put in virtual jail, ask for removal of your content (Was: SWI Agent Provocateur gets kicked out of Rocq?) Mild Shock <janburse@fastmail.fm> - 2025-11-30 12:55 +0100
csiph-web