universe level maximum integer

Stream: lean4

[Madeleine Birchfield]

What happens when you try doing mathematics in Lean at the maximum integer value used to index the universes before the integer overflow occurs?

In Agda, up until a few months ago, it was possible to prove Russell's paradox at the (2^64 - 1)th universe: https://github.com/agda/agda/issues/5706

[Henrik Böving]

docs4#Lean.Expr uses docs4#Lean.Level to represent universe levels which doesn't seem like it is prone to overflow?

[Marc Huisinga]

I haven't looked into it too closely but what about functions like to_offset?

[Gabriel Ebner]

Oh, that is indeed an issue. The function will overflow on inputs that are larger than 103 gigabytes.

[Locria Cyber]

A function that takes a bijillion years to finish is total.

[Reid Barton]

Lean takes an ultrafinitist approach to universe levels

[Julian Berman]

Madeleine Birchfield said:

In Agda, up until a few months ago, it was possible to prove Russell's paradox at the (2^64 - 1)th universe: https://github.com/agda/agda/issues/5706

This is cute :) added it to my bug collection.