Litex: Formal Math for Everyone – Set Theory Examples with Lean Comparison

Posted15 days agoActive6d ago

litexlang

13 points

3 comments

litexlang.comResearchstory

informativeneutral

Debate

20/100

Formal VerificationProof AssistantsMathematics

Key topics

Formal Verification

Proof Assistants

Mathematics

Discussion Activity

Light discussion

First comment

N/A

Peak period

156-168h

Avg / period

1.8

Key moments

01Story posted
Dec 19, 2025 at 7:25 AM EST
15 days ago
Step 01
02First comment
Dec 19, 2025 at 7:25 AM EST
0s after posting
Step 02
03Peak activity
3 comments in 156-168h
Hottest window of the conversation
Step 03
04Latest activity
Dec 27, 2025 at 8:37 AM EST
6d ago
Step 04

Generating AI Summary...

Analyzing up to 500 comments to identify key contributors and discussion patterns

Discussion (3 comments)

Showing 11 comments

tucnak

9 days ago

2 replies

The code bits are criminally unreadable in dark mode—white outlines over light gray background...

observationist

9 days ago

Almost looks like the highlight and default colors got swapped - ctrl+a to read looks ok, but oof.

litexlangAuthor

9 days ago

Thanks! It seems the font color defers in different systems (I did not find this behavior on my machine). So I changed the font color to pink :)

Happy Christmas

lupire

8 days ago

1 reply

Something that always bugged me about Lean is how unreadable and unwritable.

Math uses extremely heavy notation to make statements concise. It's hard to learn the notation without a visual reference guide, sync the symbols don't have guessable names, but once you know what the symbols mean, it's readable.

Java is incredibly verbose but you can make out what it's saying word by word

Lean is line noise. It's like assembly language for math, which is great, but not what humans should be using day to day.

This Litex does a nice job of being concerned about humans reading and writing the code.

jojomodding

8 days ago

Do you have an example Lean statement you struggle with? I would have posed that they're "just" using standard math notation that should be explained in the relevant textbook for the math you're trying to formalize, but perhaps they are indeed cooking...

markusde

8 days ago

1 reply

One thing I never understood about this: why does this not just compile to Lean so they're compatible with each other? Having a good interface is admirable, but the difference between set and type based foundations seems not very important and porting any enough math to sustain Litex seems like a huge undertaking.

litexlangAuthor

8 days ago

1 reply

It's truely great if Litex does compile to existing formal languages. The only problem is that we can not find a good way to compile our verification process, which does not require users to give names to facts they are using and thus very different from how Lean works, to Lean (set theory example is just the first one of a series of comparisons). Besides, it's even harder to compile future functionaliteies, like printing out results of each statement of litex in a human readable way, to lean. So since litex is still a young language and we are using our limited resources to try new ideas and crack here and there, for the time being we believe it's not a good time to migrate our code in such a great scale. Thank you. Merry Christmas.

markusde

6d ago

To be honest I'm not convinced by the technical downsides you mentioned here BUT I can see why you wouldn't want to spend time on this if it takes away from language development. Thanks!

gravifer

8 days ago

I would have to port this Chinese thread to HN

[如何评价 Litex 语言？ - 知乎](https://www.zhihu.com/question/1965786839827854197)

igornotarobot

9 days ago

Litex is probably closer to TLA+ than to Lean. Both draw inspiration from untyped set theory and LaTeX.

litexlangAuthor

15 days ago

[Litex](https://litexlang.com) is a simple open-source computer language for mathematical proofs. Anyone can have a rough understanding of Litex in 2 hours.

Although it is not yet ready for production use, it is already powerful enough to formalize set theory and basic logic, which is enough for most daily mathematical proofs. Visit [Set Theory Examples](https://litexlang.com/doc/How_Litex_Works/Litex_vs_Lean_Set_...) for more examples.

Star the repo [here](https://github.com/litexlang/golitex) to support Litex, and join our [Zulip community](https://litex.zulipchat.com/join/c4e7foogy6paz2sghjnbujov/) to give us feedback and suggestions!

View full discussion on Hacker News

ID: 46325073Type: storyLast synced: 12/24/2025, 10:30:23 PM

Want the full context?

Jump to the original sources

Read the primary article or dive into the live Hacker News thread when you're ready.

Open link View on HN