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

51–60 of 86 posts

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

#51

Post by litexlang »

fallat wrote: post #11
blubber wrote: post #4

How did you formally test this claim: "Even Kids can formalize the multivariate equation in Litex in 2 minutes"

Yeah, I don't think the authors _actually_ mean that. I think English isn't their first language. We should try to be charitable (but with a healthy amount of skepticism!); it's possible they meant "Even a child [with a good understanding of Litex] could [mechanically] formalize this multivariate equation in Litex in 2 minutes [as opposed to remembering and writing Lean 4 syntax]"

HAHA, thank you fallat, I guess you are right!

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

#52

Post by litexlang »

lou1306 wrote: post #35

I got kind of lost at this part of the tutorial ( https://litexlang.com/doc/Tutorial/Know ): know forall x N: x >= 47 => x >= 17 let x N: x = 47 x >= 17 How does that assumption in the first line have any effect? Surely the underlying theory of naturals should be enough to derive 47 >= 17 ? And in general I am very skeptical of the claim that Litex "can be learned by anyone in 1–2 hours". Even just the difference bet…

The first line is essential, because Litex does not implement transitivity of >= in its kernel and one has to formalize it: know @larger_equal_is_transitive(x, y, z R): x >= y y >= z

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

#53

Post by litexlang »

lou1306 wrote: post #35

I got kind of lost at this part of the tutorial ( https://litexlang.com/doc/Tutorial/Know ): know forall x N: x >= 47 => x >= 17 let x N: x = 47 x >= 17 How does that assumption in the first line have any effect? Surely the underlying theory of naturals should be enough to derive 47 >= 17 ? And in general I am very skeptical of the claim that Litex "can be learned by anyone in 1–2 hours". Even just the difference bet…

know @self_defined_axiom_larger_equal_is_transitive(x, y, z R): x >= y y >= z =>: x >= z

Since transitivity of >= is not implemented, one has to call this self_defined_axiom_larger_equal_is_transitive to make x >= 17 here, so

``` know forall x N: x >= 47 => x >= 17 ```

is essential

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

#57

Post by anonzzzies »

litexlang wrote: post #43

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 peopl…

Lisp is pretty practical even though not many people use it anymore.

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

#58

Post by lou1306 »

litexlang wrote: post #52
lou1306 wrote: post #35

I got kind of lost at this part of the tutorial ( https://litexlang.com/doc/Tutorial/Know ): know forall x N: x >= 47 => x >= 17 let x N: x = 47 x >= 17 How does that assumption in the first line have any effect? Surely the underlying theory of naturals should be enough to derive 47 >= 17 ? And in general I am very skeptical of the claim that Litex "can be learned by anyone in 1–2 hours". Even just the difference bet…

The first line is essential, because Litex does not implement transitivity of >= in its kernel and one has to formalize it: know @larger_equal_is_transitive(x, y, z R): x >= y y >= z

Thank you for clarifying, but don't you think this puts a rather big dent in the claim that Litex is "intuitive" and "can be learned by anyone in 1–2 hours"? I think the average user would expect the natural/real numbers to come equipped with this kind of theorems.

For instance, the tutorial says that "The daily properties" (whatever this means) of "+, -, , /, ^, %" are "already in the Litex kernel". What about associativity of and +, or distribution of * over +? Are these part of the "daily properties"? And if so, why didn't transitivity of >= not make the cut?

Just trying to understand the design choices here, this is very interesting.

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

#59

Post by gus_massa »

litexlang wrote: post #48
thaumasiotes wrote: post #37

Earlier quoted context omitted.

> 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 an…

How does it escale for NxN system? Let's say N=10 that is the maximal amount I'd write by hand (in exchange for a lot of money).

I took a look at the example and it's very intuitive. I'm trying to guess which heuristics is it using. Does it try to find exact matches of whatever is inside the parenthesis?

@GP?: Doesn't Lean have a "please fill the blanks" mode for short proof?

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

#60

Post by gus_massa »

teiferer wrote: post #12
blubber wrote: post #4

How did you formally test this claim: "Even Kids can formalize the multivariate equation in Litex in 2 minutes"

Kids hardly know what a multivariate equation is. Unless you use "kid" to denote 20-year old college students enrolled in a math program which some people do. The other claim is doubtful too: > while it require an experienced expert hours of work in Lean 4. No, it doesn't. If you have an actual expert, it only takes a few minutes. And besides, isn't this exactly what an artificial intelligence would solve? Take some…

I studied 2x2 linear equation system in high school at 14 (13?) y.o. It was a technical school with more math and physics, and later specialization (like chemistry, electronics, building, ...). I think in a normal school they study that at 16 y.o.

We also teach 2x2 systems to 18 y.o. in the fists year of the university for architects, medics and other degree that don't need a huge amount on math. (Other degrees like engineering or physics get 4x4 or bigger systems that definitively need the Gauss method.)

Post reply on HN