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

31–40 of 86 posts

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

#31

Post by exe34 »

teiferer wrote: post #19
exe34 wrote: post #14

Earlier quoted context omitted.

Unfortunately, whenever you try to exclude LLMs from the holy church of intelligence based on what they can't do, you end up excluding a whole lot of humans too.

That's underestimating human intelligence. Even low-IQ humans can in principle learn how to use Lean to represent a multivariate system. It might take a while, but in principle their brain is capable of that feat. In contrast, no matter how long I sit down with ChatGPT or Gemini or whatnot, it won't be able to. Because they are not intelligent. It's a great achievement of the AI hype that the burden of proof has been…

> Even low-IQ humans can in principle learn how to use Lean to represent a multivariate system.

That's an article of faith. In principle, elephants can fly at least once.

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

#32

Post by card_zero »

exe34 wrote: post #30
card_zero wrote: post #18

Earlier quoted context omitted.

Only if you're pedantic about it. I find I can arrive at all sorts of absurd conclusions like that by being extremely pedantic.

It's almost as if thinking carefully about words leads to the realisation that words are approximations that are meant to describe, not prescribe.

If "intelligence" describes LLMs then it isn't doing a very good job.

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

#33

Post by JonChesterfield »

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?

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

#35

Post by lou1306 »

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 between `have`/`let`/`know` would take a while to master. The syntax for functions is not at all intuitive (and understandably so!). & so on. The trivial subset of the language used in the README may be easy to learn but a) it would not get you very far b) most likely every other related toolbox (Lean, HOL, etc) has a similar "trivial" fragment.

But, always good to see effort in this problem space!

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

#37

Post by thaumasiotes »

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 it won't
          linear_combination 1/2 * h₁ - 3/2 * hy
        exact ⟨hx, hy⟩
---

One thing I like about the lean proof, as opposed to the litex proof, is that it specifies why the steps are correct. 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?

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

#38

Post by ngruhn »

jokoon wrote: post #21

What's a formal language?

You can write "formal" proofs in this language for mathematical theorems. They are "formal" because they are so detailed that they are machine checkable. That's in contrast to the "informal" pen and paper proofs that people normally produce.

Besides pure maths you can also use that to verify the correctness of software. E.g. say you implemented a shortest path algorithm:

   shortestPath(graph, start, end)
You could proof something like: For all `graph` and each `path` in `graph` from `start` to `end`:

    path.length

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

#39

Post by c0balt »

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…

> how are you supposed to do any nontrivial proofs?

One should also take a look at Isabelle/HOLs AFP here. You can get very far with Metis et al but it is very inefficient computationally.

Especially when proofs get larger and/or layer on abstractions (proving something nontrivial likely involves building on existing algorithms etc.) the ability to make proofs efficient to verify is important.

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

#40

Post by teiferer »

1dom wrote: post #28
teiferer wrote: post #26

Earlier quoted context omitted.

Did you read my post? The claim is "LLMs are intelligent". And instead if requiring evidence for that, apparently most folks (including you) are fine with just accepting that claim and require evidence if somebody questions this. That's what I'm doing. It's like a religion. "God exists" is the claim. Nobody needs to provide evidence that this is not the case. LLMs are intelligent" is the claim. Nobody needs to provid…

No you're not questioning it, you're making statements against it, without evidence, which is just as useless as the statement without evidence. Like I suggested, like the person you responded to suggested: when science tries to prove or disprove LLM intelligence it generally descends into disagreements about definition or evidence (neither of which you provided). The reason why no evidence was provided for the origi…

My claims:

1. LLMs are widely called "intelligent". Evidence for my claim: The term "artificial intelligence" that is used everywhere. It has its own TLD.

2. There is no evidence that this terminology is applicable. Questioning it faces some variant of "well do you have evidence to the contrary?". Evidence for my claim: This thread.

You are welcome to disprove my claims, as in the scientific spirit that you say you uphold.

Post reply on HN