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

From	Mild Shock <janburse@fastmail.fm>
Newsgroups	sci.logic
Subject	Maybe AGI should take over proving (Was: Coq/Rocq and how to completely break it)
Date	2025-07-15 18:31 +0200
Message-ID	<1055voq$293rt$1@solani.org> (permalink)
References	<104oa2l$r4na$2@dont-email.me> <104obqh$r4na$3@dont-email.me>

Show all headers | View raw

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
>

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