Lean vs Litex: Formalize irrationality of √2 and ℝ ∈ Group

Stream: general

[Jackie Shen]

Hi everyone!

I am implementing a new formal language called Litex — a simple formal language designed to make mathematical formalization accessible to everyone, even 10-year-old beginners! :rocket: With 3000+ GitHub commits and growing, Litex is now capable of handling real mathematical examples. My name is Jiachen Shen, and as a passionate language design geek, I've created Litex to bridge the gap between abstract formal systems and human intuition.

This week I implemented basic features to formalize √2 ∉ ℚ and ℝ, Z ∈ Group in Litex. Visit https://litexlang.org/playground to try the following examples. Visit my Github https://github.com/litexlang/golitex (star this repo :star: !) for more detailed introduction to Litex. Join our zulip https://litex.zulipchat.com/join/c4e7foogy6paz2sghjnbujov/ for discussions. The email is litexlang@outlook.com.

sqrt2_is_irrational.png
z_r_are_groups.png

[Wrenna Robson]

I have to say I am not fantastically convinced, having given your stuff a read.

[Wrenna Robson]

I want to meet some of these genius 10 year olds you know :)

[Eric Wieser]

In your second example, docs#Float.add_assoc not only doesn't exist, but is false

[Eric Wieser]

The web editor is handy, but I was unfortunately able to use it to show that $is_group(N, +, inverse, 0), which seems false to me

[Aaron Liu]

#eval 1e20 + -1e20 + 1e-20 == 1e20 + (-1e20 + 1e-20)

[Aaron Liu]

floats aren't very nice theoretically

[Jackie Shen]

Eric Wieser said:

In your second example, docs#Float.add_assoc not only doesn't exist, but is false

Thank you for your comment, Eric. I removed the float example. The reason why I want to prove that both ℝ and ℤ are groups is that function type narrowing is automatic in Litex, which is very convenient and uncommon in most formal languages.

[Aaron Liu]

What is function type narrowing? I suspect it might be inconsistent.

[Jackie Shen]

Wrenna Robson said:

I have to say I am not fantastically convinced, having given your stuff a read.

Thank you Robson, really appreciate your time. I will continously upload new examples and make Litex more robust and expressive in the future. LITEX IS STILL A SINGLE-HANDED PROJECT! It certainly is very far from Lean in stability, community, language maturity, etc.

As for "a 10-year-old" can understand, this is the goal of Litex and I think in some (or most?) cases, a 10-year-old has a better chance of understanding Litex code than other formal language code. Since a 10-year-old can have a sense of math, I wish one day Litex can be as easy to use as natural language.

[Jackie Shen]

Aaron Liu said:

What is function type narrowing? I suspect it might be inconsistent.

a function implements a fn_template means: 1. its domain is larger than the fn_template requirement 2. when restricted on the domain of fn_template, it satisfy all requirements of that fn_template.

There are some examples here, https://github.com/litexlang/golitex/blob/main/examples/testings/fn_template.lix . Maybe I should write some comments later? Again, thank you for your kindness and time.

[Jackie Shen]

Aaron Liu said:

#eval 1e20 + -1e20 + 1e-20 == 1e20 + (-1e20 + 1e-20)

You are right, I removed that float is group example. What I want to say is that Litex has a good system of expressing "a set of functions whose domain satisfies some requirements and return value satisfies some requirements", because the function narrowing can be automaticall checked (or checked by hand).

[Jackie Shen]

Eric Wieser said:

The web editor is handy, but I was unfortunately able to use it to show that $is_group(N, +, inverse, 0), which seems false to me

I will fix it tomorrow, thank you for your help. Really appreciate that.

[Jackie Shen]

Eric Wieser said:

The web editor is handy, but I was unfortunately able to use it to show that $is_group(N, +, inverse, 0), which seems false to me

I find the bug :( It is truly a very dumb bug. I forgot to check return value must be in the return value set specified by the fn_template. In this case, I forget i should check inverse(N) => N, which is unknown and should not be passed. Without that requirement, N "is group" is falsely correct.

[Jackie Shen]

Eric Wieser said:

The web editor is handy, but I was unfortunately able to use it to show that $is_group(N, +, inverse, 0), which seems false to me

Hi Eric, the bug is fixed. Thank you for your issue.

[kidhero]

Saw your homepage. Looks Litex aligns to the usual math language more.

[Daniel Weber]

Jackie Shen said:

Eric Wieser said:

The web editor is handy, but I was unfortunately able to use it to show that $is_group(N, +, inverse, 0), which seems false to me

Hi Eric, the bug is fixed. Thank you for your issue.

I'm not sure I understand the soundness of Litex, this seems to work:

prop is_group(s set, mul fn(s, s)s, inv fn(s)s, e s):
    forall x s, y s, z s:
        mul(mul(x, y), z) = mul(x, mul(y, z))
    forall x s:
        mul(x, inv(x)) = e
        mul(inv(x), x) = e

fn inverse(x N)N:
    inverse(x) + x = 0

forall x N:
    inverse(x) + x = 0
    x + inverse(x) = 0

$is_group(N, +, inverse, 0)

[Jackie Shen]

(deleted)

[Jackie Shen]

(deleted)

[Jackie Shen]

Daniel Weber said:

Jackie Shen said:

Eric Wieser said:

The web editor is handy, but I was unfortunately able to use it to show that $is_group(N, +, inverse, 0), which seems false to me

Hi Eric, the bug is fixed. Thank you for your issue.

I'm not sure I understand the soundness of Litex, this seems to work:

prop is_group(s set, mul fn(s, s)s, inv fn(s)s, e s):
    forall x s, y s, z s:
        mul(mul(x, y), z) = mul(x, mul(y, z))
    forall x s:
        mul(x, inv(x)) = e
        mul(inv(x), x) = e

fn inverse(x N)N:
    inverse(x) + x = 0

forall x N:
    inverse(x) + x = 0
    x + inverse(x) = 0

$is_group(N, +, inverse, 0)

Hi Daniel. The function defined here does not exist, that is why your example "falsely" works. The fn keyword in Litex does not ensure its existance (have keyword ensures).

When you define the fn function in Litex, the kernel automatically runs:

know forall prameter1 parameterSet1, ... parameterN parameterSetN: functionName( parameter1, .... , parameterN) $in ReturnSetOfThisFunction

The know keyword in Litex works like "axiom" and is not checked. That is why you can do whatever you want. In this case, you are introducing the function and making its existance as axiom.

[(deleted)]

Color me skeptical

[(deleted)]

If fn axiomatically defines a function then what is the syntax for defining a function that doesn't contradict the existing foundation

[(deleted)]

(deleted)

[Jackie Shen]

Huỳnh Trần Khanh said:

Color me skeptical

Litex have other keywords exist, have, exist_prop. exist exist_prop ensures existence. have ensures the new object is introduced with its existence ensured. In this case, for clarity of explanation, I just use the "unsafe" keyword fn as example. I am working on Litex reference manual, the detailed explanations will be on that. Thank you Khanh.

[Jackie Shen]

Huỳnh Trần Khanh said:

If fn axiomatically defines a function then what is the syntax for defining a function that doesn't contradict the existing foundation

LItex uses naive set theory (see first 4 chapters of Terry Tao's Analysis One) as foundation. The axioms ensures existance of functions, sets when they are defined properly.

[Tesla Zhang]

Here's a proof that the real number 114 is equal to the real number 514 in Litex:

prop f(x R) <=> forall y R => x = y

claim:
    forall y R => $f(y)
    prove:

claim:
    114 = 514
    prove:
        $f(514)

image.png

[Tesla Zhang]

FWIW, it does not rely on using fn to axiomatize the existence of any functions.

[KonjacSource]

He don't even know how to write a correct capture-avoiding substitution.:rolling_on_the_floor_laughing::point_right:

[Tesla Zhang]

Jackie Shen said:

@_Huỳnh Trần Khanh|511228 said:

If fn axiomatically defines a function then what is the syntax for defining a function that doesn't contradict the existing foundation

LItex uses naive set theory (see first 4 chapters of Terry Tao's Analysis One) as foundation. The axioms ensures existance of functions, sets when they are defined properly.

I don't think you can use naive set theory in a machine theorem prover, because you want to trust the logical consistency of the foundation. When it says some theorem is proved, you want to be able to trust it. Lean uses a dependent type theory with universe levels. You can also use ZFC or whatever consistent axiomatic set theory, like in Mizar.

If this is merely a LaTeX macro plus some toy proof checking, then please don't compare it with Lean. Lean is playing a completely different game here.