What's a formal language?
Litex: The First Formal Language Learnable in 1-2 Hours
21–30 of 86 posts
Re: Litex: The First Formal Language Learnable in 1-2 Hours
#22Earlier 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…
No LLM would write that without prompting it to be illiterate in English.
Re: Litex: The First Formal Language Learnable in 1-2 Hours
#23LiteX has been a digital SOC IP library for man years.
Re: Litex: The First Formal Language Learnable in 1-2 Hours
#24This 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?
The tutorial explains the language in much more detail: https://litexlang.com/doc/Tutorial/Introduction
Re: Litex: The First Formal Language Learnable in 1-2 Hours
#25Earlier 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…
> Here I am, having to defend my claim that they are not intelligent.
It's because all you've done is made a claim without any evidence. Someone pointed out a challenge that most claims about them not being intelligent can't submit any evidence that can't also be met by an LLM.
But instead of submitting any evidence to support your claim, you descended into hyperbole about how hard done by you are being expected to support your claims.
In science, it's okay to say we don't know. The amount of disagreement - even amongst smart people - about if LLMs are intelligent or not, suggest to me that we just don't have universally accepted research and definitions that are tight enough to decisively say.
But you're talking not only like you _know_ the answer for sure, so much that you don't need to support it with evidence or credentials, because those who disagree are obviously just poor victims of the AI hype machine.
Please make sure you pass your knowledge of your LLM discoveries onto the scientific community, you could change the world!
Re: Litex: The First Formal Language Learnable in 1-2 Hours
#26Earlier quoted context omitted.
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…
> Here I am, having to defend my claim that they are not intelligent. It's because all you've done is made a claim without any evidence. Someone pointed out a challenge that most claims about them not being intelligent can't submit any evidence that can't also be met by an LLM. But instead of submitting any evidence to support your claim, you descended into hyperbole about how hard done by you are being expected to s…
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 provide evidence against that. In either case, the burden of proof is with the one making the claim.
> In science, it's okay to say we don't know
But that's not what's happening. LLMs are called "AI". You know what the I stands for, right? It's not "artificial we-don't-know-if-intelligent".
Re: Litex: The First Formal Language Learnable in 1-2 Hours
#27currently reading through the tutorial. don't have much experience with coq, lean and friends, but this looks like a nice language to get started with formal proofs.
Re: Litex: The First Formal Language Learnable in 1-2 Hours
#28Earlier quoted context omitted.
> Here I am, having to defend my claim that they are not intelligent. It's because all you've done is made a claim without any evidence. Someone pointed out a challenge that most claims about them not being intelligent can't submit any evidence that can't also be met by an LLM. But instead of submitting any evidence to support your claim, you descended into hyperbole about how hard done by you are being expected to s…
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 original LLMs are intelligent claim is because - if you read through this thread - you were the first to make that claim, and the counter claim.
> But that's not what's happening. LLMs are called "AI". You know what the I stands for, right? It's not "artificial we-don't-know-if-intelligent".
I don't know what you want me to say here - if you want to continue acting like there's some widely accepted and agreed on definition of intelligence that everyone who isn't you is an idiot for not knowing, then carry on.
I don't have a reliable definition for intelligence. Like I said, if you do, please share your finding with science, you could settle some fairly big debates and change the world in a meaningful way.
Re: Litex: The First Formal Language Learnable in 1-2 Hours
#29How did you formally test this claim: "Even Kids can formalize the multivariate equation in Litex in 2 minutes"
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-th...
Re: Litex: The First Formal Language Learnable in 1-2 Hours
#30Earlier 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.
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.