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...

-Julio

--- SoupGate-Win32 v1.05
* Origin: fsxNet Usenet Gateway (21:1/5)

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)

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)