The Signal Collapse gives us System Uncertainty (Was: Having 2544 issues is probably a bad sign)

From	Mild Shock <janburse@fastmail.fm>
Newsgroups	sci.logic
Subject	The Signal Collapse gives us System Uncertainty (Was: Having 2544 issues is probably a bad sign)
Date	2025-07-15 19:01 +0200
Message-ID	<10561gu$2953g$1@solani.org> (permalink)
References	<104oa2l$r4na$2@dont-email.me> <104obqh$r4na$3@dont-email.me> <1055voq$293rt$1@solani.org> <1055vv3$2940k$1@solani.org>

Show all headers | View raw

Hi,

1. Everybody’s a programmer now
    The barrier to entry dropped dramatically — you can
    become a "developer" with a few online tutorials
    and a GitHub account.

2. Everybody’s an academic now
    Academia expanded, but standards often fell. In
    some places, it's publish or perish, so paper
    mills and fake research flourish.

3. Signal Collapse ↔ Systemic Uncertainty
    Credentials lose meaning, No reliable markers of
    skill, Fragile systems built on shallow knowledge

4. Signal Collapse ↔ Systemic Uncertainty
    Quantity overwhelms quality, Important truths get
    buried, Bad signals drown good ones

Etc..

Bye

Mild Shock schrieb:
> 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
>>>
>>
>

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