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

11–20 of 86 posts

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

#11

Post by fallat »

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]"

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

#12

Post by teiferer »

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 complex system and derive something from it. That's exactly what intelligence is about. But LLMs can't deal with the complex but very logical (by definition) and unambiguous system like Lean so we need to dumb it down.

Turns out, LLMs are not actually intelligent! We should stop calling them that. Unfortunately, there are too many folks in our industry following this hyped-up terminology. It's delusional.

Note that I'm not saying LLMs are useless. They are very useful for many applications. But they are not intelligent.

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

#13

Post by card_zero »

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.

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

#14

Post by exe34 »

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…

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.

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

#16

Post by tux3 »

Almondsetat wrote: post #10
jasonjmcghee wrote: post #8

Earlier quoted context omitted.

I doubt it? And if it is, honestly best LLM readme I've seen. What makes you think so?

>Litex(website) is a simple, intuitive, and open-source formal language for coding reasoning (Star the repo!). 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 humans and AI is Litex's core mission. This is how Li…

Humans are perfectly capable of doing that on their own. The random parentheticals and the sentence structures are very human to me.

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

#17

Post by [deleted] »

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…

[deleted]

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

#18

Post by card_zero »

exe34 wrote: post #14
teiferer wrote: post #12

Earlier quoted context omitted.

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…

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.

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

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

#19

Post by teiferer »

exe34 wrote: post #14
teiferer wrote: post #12

Earlier quoted context omitted.

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…

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 reversed. Here I am, having to defend my claim that they are not intelligent. But the burden of proof should be on those claiming intelligence. The claim that earth is a sphere was extraordinary and needed convincing evidence. The claim that species have evolved through evolution was. But the claim that LLMs are intelligent is so self-evident that rejecting the idea needs evidence? That's upside-down!

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

#20

Post by card_zero »

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…

IDK, they look intelligent, like the world looks flat.
Post reply on HN