8 ms·

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

fallat 1y ago
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]"
- litexlang 1y ago
  HAHA, thank you fallat, I guess you are right!
teiferer 1y ago
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.
- exe34 1y ago
  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.
  - card_zero 1y ago
    Only if you're pedantic about it. I find I can arrive at all sorts of absurd conclusions like that by being extremely pedantic.
    - exe34 1y ago
      It's almost as if thinking carefully about words leads to the realisation that words are approximations that are meant to describe, not prescribe.
      - card_zero 1y ago
        If "intelligence" describes LLMs then it isn't doing a very good job.
        exe34 1y ago
        try the bottom half of the population!
  - teiferer 1y ago
    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!
    - card_zero 1y ago
      IDK, they look intelligent, like the world looks flat.
- deleted 1y ago
  [deleted]
- gus_massa 1y ago
  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.)
  - teiferer 1y ago
    And if you ask one of those medics 5 years later to solve one, the response might make you depressed. (Or just 4 weeks after their maths exam.)
Dilettante_ 1y ago
Reminded me of that article about hoobastanking the Snarfus from a couple days back[1]. And xkcd 2501, of course. [1]https://anniemueller.com/posts/how-i-a-non-developer-read-the-tutorial-you-a-developer-wrote-for-me-a-beginner https://anniemueller.com/posts/how-i-a-non-developer-read-th...

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

litexlang 1y ago
HAHA, thank you fallat, I guess you are right!

teiferer 1y ago

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.

exe34 1y ago
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.
- card_zero 1y ago
  Only if you're pedantic about it. I find I can arrive at all sorts of absurd conclusions like that by being extremely pedantic.
  - exe34 1y ago
    It's almost as if thinking carefully about words leads to the realisation that words are approximations that are meant to describe, not prescribe.
    - card_zero 1y ago
      If "intelligence" describes LLMs then it isn't doing a very good job.
      - exe34 1y ago
        try the bottom half of the population!
- teiferer 1y ago
  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!
  - card_zero 1y ago
    IDK, they look intelligent, like the world looks flat.
deleted 1y ago
[deleted]
gus_massa 1y ago
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.)
- teiferer 1y ago
  And if you ask one of those medics 5 years later to solve one, the response might make you depressed. (Or just 4 weeks after their maths exam.)

Dilettante_ 1y ago

Reminded me of that article about hoobastanking the Snarfus from a couple days back[1]. And xkcd 2501, of course. [1]https://anniemueller.com/posts/how-i-a-non-developer-read-the-tutorial-you-a-developer-wrote-for-me-a-beginner https://anniemueller.com/posts/how-i-a-non-developer-read-th...