Hacker News Board Hacker News, browsed like a classic message board
Live data from Hacker News

Litex: The First Formal Language Learnable in 1-2 Hours

github.com

Post reply on HN
Print view View original

41–50 of 86 posts

Re: Litex: The First Formal Language Learnable in 1-2 Hours

#41

Post by Someone »

jokoon wrote: post #21

What's a formal language?

The only definition I know of is https://en.wikipedia.org/wiki/Formal_language. I also think that is the commonly accepted definition.

Taking that as the definition, this definitely is not the first formal language learnable in 1-2 hours. I would think, for example, that the language consisting of just the empty string is older and learnable in 1-2 hours.

They probably mean something like “formal language used for writing mathematical proofs that is (about) as powerful as Lean”, though.

Re: Litex: The First Formal Language Learnable in 1-2 Hours

#42

Post by CaptainOfCoit »

ccppurcell wrote: post #7

"Never believe quote attributions given on the internet" - Abraham Lincoln

The quote from the README seems indeed to be falsely attributed to da Vinci. The quote in question:

> Simplicity is the ultimate sophistication. - Leonardo da Vinci

https://checkyourfact.com/2019/07/19/fact-check-leonardo-da-...

https://quoteinvestigator.com/2015/04/02/simple/

I'm not sure why people don't spend two minutes looking up a quote before sharing it, feels like most people have zero care about quality or polish today, everything is half-assed.

Re: Litex: The First Formal Language Learnable in 1-2 Hours

#43

Post by litexlang »

Hi there! I am jiachen shen, creator of Litex.

I feel really lucky that Litex has drawn so much attention from you guys! I always like the geek culture of HN, and have absolutely no idea why such a random guy from a random background can rush into the top 10 on Hacker News.

Litex gets its name from Lisp and LaTeX. I want to make Litex as elegant and deep as Lisp, and at the same time as pragmatic as LaTeX.

Many people have raised questions and suggestions about Litex, and I’m truly grateful. Since I’m developing the Litex core on my own, a lot of the documentation is still incomplete — I’ll try my best to improve it soon! All of your suggestions are really helpful. Thank you so much!

Re: Litex: The First Formal Language Learnable in 1-2 Hours

#44

Post by litexlang »

JonChesterfield wrote: post #33
litexlang wrote: post #2

Litex is a simple, intuitive, and open-source formal language for coding reasoning (Star the repo! https://github.com/litexlang/golitex ). It ensures every step of your reasoning is correct, and is actually the first reasoning formal language (or formal language for short) that can be learned by anyone in 1–2 hours, even without math or programming background. Making Litex intuitive to both human and AI is the missio…

The website tells me it's simple over and over but not what it is. What're the semantics? Which mathematical system is this? What can it prove?

Thank you Jon, I will put the semantics and the mathematical system behind online soon! Just give me some time!

Re: Litex: The First Formal Language Learnable in 1-2 Hours

#45

Post by CaptainOfCoit »

ngruhn wrote: post #36
aktuel wrote: post #27

currently reading through the tutorial. don't have much experience with coq, lean and friends, but this looks like a nice language to get started with formal proofs.

fyi: they finally renamed Coq. It's called Rocq now.

Guess they had to change the logo too? Just because evangelical anglophone users couldn't get past the name sounding like "cock" or what?

Re: Litex: The First Formal Language Learnable in 1-2 Hours

#46

Post by litexlang »

CaptainOfCoit wrote: post #42
ccppurcell wrote: post #7

"Never believe quote attributions given on the internet" - Abraham Lincoln

The quote from the README seems indeed to be falsely attributed to da Vinci. The quote in question: > Simplicity is the ultimate sophistication. - Leonardo da Vinci https://checkyourfact.com/2019/07/19/fact-check-leonardo-da-... https://quoteinvestigator.com/2015/04/02/simple/ I'm not sure why people don't spend two minutes looking up a quote before sharing it, feels like most people have zero care about quality or p…

Thank you captain! Your observation is pretty interesting! I will fix that after I have more information!

Re: Litex: The First Formal Language Learnable in 1-2 Hours

#47

Post by litexlang »

thaumasiotes wrote: post #37
litexlang wrote: post #2

Litex is a simple, intuitive, and open-source formal language for coding reasoning (Star the repo! https://github.com/litexlang/golitex ). It ensures every step of your reasoning is correct, and is actually the first reasoning formal language (or formal language for short) that can be learned by anyone in 1–2 hours, even without math or programming background. Making Litex intuitive to both human and AI is the missio…

> Even Kids can formalize the multivariate equation in Litex in 2 minutes, while it [takes] an experienced expert hours of work in Lean 4. Well, I propose an alternative proof in lean4: import Mathlib.Tactic example (x y : ℝ) (h₁ : 2 * x + 3 * y = 10) (h₂ : 4 * x + 5 * y = 14) : x = -4 ∧ y = 6 := by have hy : y = 6 := by linear_combination 2 * h₁ - h₂ have hx : x = -4 := by -- you'd think h₁ - 3 * hy would work, but…

Thank you thau! Your example is pretty interesting! I avoid using any advanved Mathlib tactic to make the comparison fairer. We are comparing Lean and Litex under conditions where they don’t rely too much on external packages, which makes the comparison a bit fairer. (since Lean does have a very rich set of libraries, but building libraries is itself a challenge. Litex really needs to learn from Lean on how to build a successful library!).)(afterall, Litex can also abstract all proofs here and give it a name linear_combination, right?)

Re: Litex: The First Formal Language Learnable in 1-2 Hours

#48

Post by litexlang »

thaumasiotes wrote: post #37
litexlang wrote: post #2

Litex is a simple, intuitive, and open-source formal language for coding reasoning (Star the repo! https://github.com/litexlang/golitex ). It ensures every step of your reasoning is correct, and is actually the first reasoning formal language (or formal language for short) that can be learned by anyone in 1–2 hours, even without math or programming background. Making Litex intuitive to both human and AI is the missio…

> Even Kids can formalize the multivariate equation in Litex in 2 minutes, while it [takes] an experienced expert hours of work in Lean 4. Well, I propose an alternative proof in lean4: import Mathlib.Tactic example (x y : ℝ) (h₁ : 2 * x + 3 * y = 10) (h₂ : 4 * x + 5 * y = 14) : x = -4 ∧ y = 6 := by have hy : y = 6 := by linear_combination 2 * h₁ - h₂ have hx : x = -4 := by -- you'd think h₁ - 3 * hy would work, but…

``` If litex's strategy is "you describe the steps you want to take, and litex will automatically figure out why they're correct", how are you supposed to do any nontrivial proofs? ```

HAHA, what i am saying here is, each statement you write, is automatically checked by Litex, using its known specific facts and universal facts. Since any math proof, no matter complex or simple, can be divided into many small steps and each small step can be verified in that way, I guess it is fair to say "automatically figure out why they're correct" to a non-mathematicl person when introducing Litex.

Re: Litex: The First Formal Language Learnable in 1-2 Hours

#49

Post by litexlang »

card_zero wrote: post #13
two_handfuls wrote: post #9

This looks potentially interesting. The "cheat sheet" seems the most useful document listed but it lost me there: > Use `have` to declare an object with checking its existence. an object with what?

With checking-its-existence. With checking of its existence. With existence checking. While checking its existence. OK it could be better written.

haha, you are right bro!

Re: Litex: The First Formal Language Learnable in 1-2 Hours

#50

Post by litexlang »

two_handfuls wrote: post #9

This looks potentially interesting. The "cheat sheet" seems the most useful document listed but it lost me there: > Use `have` to declare an object with checking its existence. an object with what?

have is used to ensure the existence of the object you define. For example, you do not want to declare a new object when it is from an empty set!
Post reply on HN