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

71–80 of 86 posts

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

#71

Post by teiferer »

mkl wrote: post #61
teiferer wrote: post #40

Earlier quoted context omitted.

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

> The term "artificial intelligence" that is used everywhere. It has its own TLD. That's the country code TLD for Anguilla: https://en.wikipedia.org/wiki/.ai

Sure. The top 100 domains with that TLD still have little to do with Anguilla.

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

#72

Post by thaumasiotes »

litexlang wrote: post #47
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…

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…

> Your example is pretty interesting! I avoid using any advanved Mathlib tactic to make the comparison fairer.

I learned about the `linear_combination` tactic from your example. Other than that, I use `have` and `exact`, which (a) are not advanced, and (b) are also used in your example.

Before that, my first attempt at the lean proof looked like this:

    example (x y : ℝ)
        (h₁ : 2 * x + 3 * y = 10)
        (h₂ : 4 * x + 5 * y = 14)
        : x = -4 ∧ y = 6 := by
          -- double h₁ to cancel the x term
          have h₃ : 2 * (2 * x + 3 * y) = 2 * 10 := by rw [h₁]
          conv at h₃ => ring_nf -- "ring normal form"
          -- subtract h₂ from h₃
          have h₄ : (x * 4 + y * 6) - (4 * x + 5 * y) = 20 - 14 := by rw [h₂, h₃]
          conv at h₄ => ring_nf
          conv at h₁ =>
            -- substitute y = 6 into h₁
            rw [h₄]
            ring_nf
          -- solve for x
          have h₅ : ((18 + x * 2) - 18) / 2 = (10 - 18) / 2 := by rw [h₁]
          conv at h₅ => ring_nf
          apply And.intro h₅ h₄
> We are comparing Lean and Litex under conditions where they don’t rely too much on external packages

This proof does have the advantage of not needing to import Mathlib.Tactic. Although again, that's something your proof does.

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

#73

Post by thaumasiotes »

gus_massa wrote: post #59
litexlang wrote: post #48

Earlier quoted context omitted.

``` 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?

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

Yes, there are several depending on what you want to do. The catchall is `simp` (short for 'simplify').

Why do we need more than one "do what I mean" command? (Or more than zero "do what I say" commands?) Because it's impossible to know what you mean. If you try to use a lot of `simp`, you'll notice that you often have to tell it what to do.

Note that what we really want for this problem is a linear algebra package that can do row reduction, not a formal prover. This problem is all arithmetic.

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

#74

Post by exe34 »

teiferer wrote: post #70
exe34 wrote: post #63

Earlier quoted context omitted.

the way it goes is that a device/program of some sort displays a broad number of behaviours that previously was believed to be a future sign of artificial intelligence (e.g. somewhat coherent text, Turing test, giving the impression of following instructions and arriving at the correct results, etc). some people claim this is artificial intelligence of a lower quality than humans, and these people expect that such me…

> my point was that every time you try to say that no this can't be what intelligence means, it needs to do X, I can find a human who can't do X, Indeed, the point you are making is reasonable. But I'm trying to say that the premise is wrong. Nobody should be expected to come up with a reason why it is not intelligence. We should expect to be presented with evidence that it is intelligence. Absent that, the null hypo…

>Nobody should be expected to come up with a reason why it is not intelligence.

I'm not asking anybody to come up with a reason why it's not intelligence. I'm telling people they're wrong when they do try to justify calling it not intelligent. if you want to gatekeep a word, you should at least try to define it and then stick to the definition.

It is intelligence in the sense that if somebody had described it in 2010, we would have said yes, that's intelligence and it's hundreds of years away. It isn't intelligence in the sense that it's now here and we've found holes in the story.

Intelligence is so poorly defined that it's an ever receding finish line that somehow we're supposed to cross before we can call the device intelligent.

As Dennett said, it's like magic. Magic that is possible is just tricks. Real magic is that which is impossible.

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

#78

Post by Smoosh »

cbdevidal wrote: post #34
ccppurcell wrote: post #7

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

“Arrrg! I’ve seen that quote everywhere! I must put a stop to this.” - John Wilkes Booth

“I believe John Wilkes Booth to be innocent!” - Alexander Hamilton.

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

#79

Post by majorchord »

almostgotcaught wrote: post #77
tverbeure wrote: post #75

Earlier quoted context omitted.

That’s a lot of words and anger for such a small thing.

It's a low brow dismissal of someone's work? How else should I react?

this might shed some light on what's wrong: https://0x0.st/KB-b.txt

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

#80

Post by almostgotcaught »

majorchord wrote: post #79
almostgotcaught wrote: post #77

Earlier quoted context omitted.

It's a low brow dismissal of someone's work? How else should I react?

this might shed some light on what's wrong: https://0x0.st/KB-b.txt

> Hacker News users don’t see you...

Lolol I sure hope no one hn sees me as anything (otherwise it's past due for me to dump this handle).

Post reply on HN