Newsportal USENET - Maybe AGI should take over proving (Was: Coq/Rocq and how to completely break it)

Sujet : Maybe AGI should take over proving (Was: Coq/Rocq and how to completely break it)
De : janburse (at) *nospam* fastmail.fm (Mild Shock)
Groupes : sci.logic
Date : 15. Jul 2025, 17:31:23

Autres entêtes

Message-ID : <1055voq$293rt$1@solani.org>
References : 1 2
User-Agent : Mozilla/5.0 (Windows NT 10.0; Win64; x64; rv:128.0) Gecko/20100101 Firefox/128.0 SeaMonkey/2.53.21

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

Date	Sujet	#	Auteur
10 Jul 25	Coq/Rocq and how to completely break it	5	Julio Di Egidio
10 Jul 25	Re: Coq/Rocq and how to completely break it	4	Julio Di Egidio
15 Jul17:31	Maybe AGI should take over proving (Was: Coq/Rocq and how to completely break it)	3	Mild Shock
15 Jul17:34	Having 2544 issues is probably a bad sign (Was: Maybe AGI should take over proving)	2	Mild Shock
15 Jul18:01	The Signal Collapse gives us System Uncertainty (Was: Having 2544 issues is probably a bad sign)	1	Mild Shock