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
--- SoupGate-Win32 v1.05
* Origin: fsxNet Usenet Gateway (21:1/5)