Litex: Formal math for everyone with set theory examples

Stream: general

[Jackie Shen]

Litex is an open-source proof language aimed at making formal mathematics more approachable. Its design emphasizes a low entry barrier: with basic mathematical background, one can understand the core syntax and workflow in a short time.

Visit Set Theory Examples for more explanation.

While Litex is not intended as a replacement for professional proof assistants, it can be viewed as a lightweight step toward formalization, especially for learning, experimentation, or small-scale developments. It is already expressive enough to formalize simple set-theoretic arguments and toy examples. A comparison with Lean in the context of set theory is available in the documentation.

web: https://litexlang.com
Star the repo here to support Litex
Join our Zulip community to give us feedback and suggestions :)

Really thank the supportors from lean group. wish lean community a brighter future.

Here are some of the examples:

截屏2025-12-19 20.34.01.png
截屏2025-12-19 20.34.08.png
截屏2025-12-19 20.34.15.png
截屏2025-12-19 20.34.33.png
截屏2025-12-19 20.34.45.png
截屏2025-12-19 20.34.53.png
截屏2025-12-19 20.35.03.png
截屏2025-12-19 20.35.10.png
截屏2025-12-19 20.35.20.png

[Johan Commelin]

I just picked a random example:

import Mathlib

example : {n : ℕ | n ≥ 5 ∧ n < 8} = ({5, 6, 7} : Finset ℕ) := by grind

[Haoyang Shi]

seems good :tada:

[Jackie Shen]

Johan Commelin said:

I just picked a random example:

import Mathlib

example : {n : ℕ | n ≥ 5 ∧ n < 8} = ({5, 6, 7} : Finset ℕ) := by grind

Thanks! i will update my example in my web :) Your example really shows the power of mathlib :)

[Johan Commelin]

I haven't tried the others, but I'm guessing they can also be golfed.

[Jackie Shen]

Johan Commelin said:

I haven't tried the others, but I'm guessing they can also be golfed.

Sure! My example sort of is comparing vanilla lean with vanilla litex. It is possible to enclose some logic in lean in my examples and make lean examples shorter :)

[Julian Berman]

Previous discussions in #general > Lean vs Litex: Formalize irrationality of √2 and ℝ ∈ Group and #general > Litex: The ‘Too Easy’ Formal Language Even Kids Can Master

[liao zhang]

Good work!

[Vlad Tsyrklevich]

Are the obvious sock puppets necessary?

[Jackie Shen]

Julian Berman said:

Previous discussions in #general > Lean vs Litex: Formalize irrationality of √2 and ℝ ∈ Group and #general > Litex: The ‘Too Easy’ Formal Language Even Kids Can Master

thank you for your comment! litex has undertaken drastic update in the few months by listening to feedbacks from the community. we updated how it expresses this example in a stricter way. now i guess it is right time to update our progress and learn from lean community after 3 months. again thank you for your time.

[Xiyu Zhai]

Congratulations

[Xiyu Zhai]

Johan Commelin said:

I just picked a random example:

import Mathlib

example : {n : ℕ | n ≥ 5 ∧ n < 8} = ({5, 6, 7} : Finset ℕ) := by grind

I've been saying this a while ago. Lol. Lean's grind is quite strong. And you can easily write much stronger tactics by building upon it.

[Jackie Shen]

Xiyu Zhai said:

Johan Commelin said:

I just picked a random example:

import Mathlib

example : {n : ℕ | n ≥ 5 ∧ n < 8} = ({5, 6, 7} : Finset ℕ) := by grind

I've been saying this a while ago. Lol. Lean's grind is quite strong. And you can easily write much stronger tactics by building upon it.

Thanks :) grind is a really powerful tactic of course! I am wondering whether tactics like grind can fundamentally solve all of the set-related gap between how people usualy think and how we express such math expressions in lean, especially when it comes to the fact that any object in Lean can only belong to one type, while objects can actually belong to infinitely different sets. Looking for your professional feedback!