lutusp

This will come in handy after AI takes over the world.

But kidding aside, this is an interesting reveal on the ease with which a custom LLM can be spun up to fit a particular niche application, especially for systems not meant to host an LLM.

> No, the claims they made are well supported.

Here's the claim:

> Ideally, such techniques could find and patch all bugs, and then provide some proof that there are no more to be found.

The claim "Find and patch all bugs" is false. This is computer science 101. It is not possible. All one can say is that the claims are well-repeated. They aren't supported at all.

> You can see that the blog post does not claim to solve the halting problem;

Yes, true, they just ignored it and made unsupportable claims. And the Halting Problem cannot be "solved," that is what the Halting Problem says and proves.

> The language is Turing-complete, not the program.

That means we can't make the claim that a particular program, running in that language, is error-free. I don't get why people find this so hard to understand.

> That would imply you could never know anything about a program.

No, it means we can't make the claim that a program is error-free. That's the simplest statement of the Halting Problem.

When someone applies Lean to verify the correctness of a chain of logic, they must remember than Lean cannot be proven to be error-free, because ... wait for it .. Lean is Turing-complete.

This is an excellent study/article/whatever. Its combination of cartoons and aphorisms is spookily good.

Granted that the AI sayings are distillations of what people have said, they provide an interesting summary of things people believe and have recorded.

> The halting problem applies when you are trying to check the properties of arbitrary programs. However, we are not writing arbitrary programs, we are writing very specific (hopefully useful) programs. The two are very different.

No, they aren't -- they are all Turing-complete, look it up. The THP applies to all non-trivial programs, meaning programs that support Peano arithmetic or anything more involved. That limitation certainly applies to all the programs you're describing.

> Pop-sci explanations of the halting problem have probably done incredible damage to formal verification as a whole.

That's pretty funny. It's not every day I hear Alan Turing and Kurt Gödel described as purveyors of "pop-sci".

> Mostly because it makes people with only the most cursory understanding of it go "why bother, it won't work anyway."

I won't try to list all the logical fallacies in your argument. You could do that if you were so inclined.

> Ideally, such techniques could find and patch all bugs, and then provide some proof that there are no more to be found.

I wish people would learn a little computer science before making this kind of impossible claim. And I wonder how many people read claims like this and accept them without investigation.

The Turing Halting Problem (THP) invalidates the above claim, on all nontrivial software systems, forever.

The THP (1937) is derived from Gödel's Incompleteness Theorems (1931), and the latter are not a matter of opinion.

For those with limited attention spans, ask yourself this: How does the foolproof program checker check itself?

Grant Sanderson tries to explain why getting into math remains worthwhile in an AI era. But his audience is composed of two groups -- people who won't follow his reasoning, and mathematicians.

Someone once described a mathematician as a machine to turn coffee into theorems. Okay, fair enough, but what sets mathematicians apart is that mathematics wasn't a choice.

It's possible that Sanderson doesn't get this, but people watching his video either will never understand his argument, or have always understood it.

> But why can't a hyper-intelegent [sic] AI ...

Well, this was definitely not written by AI.

> ... it's like if we had an explaination [sic] of ...

I hear that running a spell-checker is no longer a sin.

Here's the title of the HN submission:

"TV4 postpones show after AI agent erases edited material"

Here's the title of the original article:

"TV4 postpones The Challenge after backup failure forces season to be edited again"

The claim that AI was involved is contradicted by the article itself: “It is not true that some independent AI agent went in and deleted the material,” says Mia Lindqvist, program director at TV4.

This kind of submission tells us more about the submitter's views than about the events themselves.

> ... It’s a position tailored to dissuade prosecution as it removes intent, which is typically required for a crime.

Don't forget negligence. Much of criminal law hinges on failing an implied or explicit responsibility. Negligence would propel a prosecution in many similar contexts, but AI is so new that little prior case law exists. Oh, and IANAL.

The key to this story is in the word "liable." That's lawyer-speak for a civil, not criminal, legal judgment. The loser must pay money, no one goes to jail, and Meta has so much money that the judgment means nothing.

Meta already pays billions to gain access to people's personal data. This is just another business expense, a line item on a balance sheet.

When faced with an adverse ruling, an individual raises his hands, is handcuffed and led away. A corporation raises its prices.

> Church and Turing did not prove their papers with the words,

THAT STATEMENT IS FALSE. The two articles used DIFFERENT EQUATIONS TO SUPPORT THE SAME LOGICAL ARGUMENT. Church and Turing are jointly credited with the same logical conclusion, even though they used different mathematical arguments. NO ONE said, "Wait, the equations are different, therefore the conclusion must be different." At least no one with an education.

> ... they described the math proving their statements in them and what that math implies (which is why the ending summary would not be math, it must already have been shown to be a summary).

Church and Turing made the same logical claim, using the same words but different mathematical arguments. This places the math in a supporting role, below logical reasoning. This is true in all the examples I provided. Math is a language, but to use it, you must have something to say.

In the Relativity example I gave, Einstein's math teacher used the SAME equation to draw a DIFFERENT CONCLUSION, because EQUATIONS SUPPORT IDEAS, THEY AREN'T THEMSELVES IDEAS.

Just as with words, math equations never stand by themselves -- they support ideas, and the same idea can be expressed by different mathematical arguments. That was the point of all my examples, which clearly fell on the ears of a religious true believer.

This equation -- y = sqrt(1-x*x) -- can be taken to mean (a) pi/4 if integrated on the interval 0 < x < 1, or (b) space and time are separate dimensions, which is what Minkowski noticed and Einstein didn't. But by itself, THE EQUATION MEANS PRECISELY NOTHING -- for that, you must have ideas.

If you possessed the intellectual integrity of the average 12-year-old, you would realize that using the same words as Ernest Hemingway doesn't make you a great writer, and using the same equations as Einstein doesn't make you an original thinker. That requires ideas, not equations.

I post this for the benefit of other readers, who unlike you might have some depth of understanding, some grasp of the relation between ideas and equations.

> The executive assumed that we were competent, and was saying "I already believe you. Now let's talk about what happens next".

Apropos, I was once told a Japanese saying: "Fix the problem, not the blame."

I must have repeated this charming story a dozen times before realizing it makes no sense in Japanese -- it relies entirely on English idioms.

>> There are plenty of equations, but the paper's meaning lies in its logical arguments

> This is the difference I feared. I trust, understand, and take lead of the rigorous math of the paper, you opt to follow in English arguments of what you think it's supposed to mean or apply to.

Excuse me? The articles don't prove their theses with mathematics, they prove them with logic. Equations are assistants, but they're entirely replaceable, as proven by the fact that Church and Turing used different equations in support of their theses -- articles that come to the same conclusion.

How did you miss the significance of the Alonso Church article's final sentence: "The general case of the Entscheidungsproblem of the engere Funktionenkalkül is unsolvable." Where are the equations that you think make the point better than these words? Certainly not in the article. Why didn't Church refer to an equation to support his conclusion? The answer is that his conclusion is a logical one, not a mathematical one.

In the case of Navier–Stokes, the equation is a preliminary, a self-evident statement about energy, inertia, pressure and a few other things. If it were rewritten (as it often is), the problem remained to be solved. Those who solved it didn't post a new equation, they posted a new insight.

In the relativity example, Einstein wrote an equation but didn't understand it -- his math teacher took over. Any number of equivalent expressions would have provided a basis for progress toward a more comprehensive theory. The point was the ideas, not the equations.

> ... the rigorous math of the paper ...

Nonsense. In both papers, the authors use mathematics only to support their points, in the same way that an author uses words to craft a story. If separated from the logical thread, the words (the equations) lose all meaning. This is proven by the fact that the two papers use different mathematics to support the same thesis.

But I see I'm wasting my time. Mathematics is a language, but to use it, you must have something to say.