> This is a simple restatement of the original claim, and it is false. The program being discussed is subject to the Turing Halting Problem. The program being tested, the same. Lean, the prover and the final authority, the same. All are subject to this fundamental limitation.
I disagree, which is why I added all of the additional commentary you appear to have ignored to restate your original claim instead. I'm not sure why I should restate my response to these points when they're still available and awaiting response above.
> How the original author chose to express himself is not my problem, it is his. I have the simple responsibility to take him at his word. Anything else would be disrespectful.
When someone's words on a project as complicated as this seems to violate the basic foundations of computer science it's both your problem & disrespectful to claim you know for certain the problem is because it's a common beginners mistake. This may be something we cannot come to an agreement on morally, but I suppose it won't really matter for the rest of the mathematical conversation which continues below.
> I didn't define it, Alan Turing did, in 1936. It's not a debating point, it's a fundamental limitation. All Turing-complete code sources have this limitation. Read more here: https://en.wikipedia.org/wiki/Halting_problem .
Wikipedia is a poor source to cite, but when I follow it I see no claim or definition by Turing for what non-trivial is. I see claim of what Rice meant by non-trivial in their eponymous theorem in 1951, but that's neither from 1936 nor a relevant definition for the current discussion so I must assume you mean somewhere else in Turing's actual paper I'd need to check.
Which takes us to the actual 1936 paper rather than Wikipedia's summary https://www.cs.virginia.edu/~robins/Turing_Paper_1936.pdf. I see 3 mentions of triviality, none of which appear to give a definition of what a non-trivial provably haltable example is:
1. Discussion of the remainder of the theorem itself being trivial [on page 31 of his paper, page 260 of the journal]
2. Since CC_0 is already been shown provable the conditional proof of the A(M)->CC_0 is trivial by the rules of implication [p32, 261 of the journal]
3. A trivial replacement of the variable naming scheme allows translation between the two notations without changing the calculus of them. [p34, 263 of the journal]
None of these seem to define what a non-trivially provable program (Turing Machine/Algorithm) is in context of the halting problem, so I again ask can you tell me where and what actual definition in Turing's actual 1936 paper you are using to define what a non-trivial program is so that I may apply this definition to the current conversation?
As another aside, one of my favorite "simplest" examples of a non-trivially provable program we know never halts despite the general case result of the halting problem:
for every group of positive integers (a,b,c,n) with n > 2:
if a^n + b^n = c^n:
halt
To prove this never halts you have to prove Fermat's last theorem. Which we have, and so we know this must never halt as you iterate infinitely over the positive integers, but it took one of the most complicated mathematical proofs known to show it.
There are certainly definitions of non-trivial where this is still considered trivial, but I'm at a loss to what part of Turing's paper gives such a definition.
>> This is a simple restatement of the original claim, and it is false. The program being discussed is subject to the Turing Halting Problem. The program being tested, the same. Lean, the prover and the final authority, the same. All are subject to this fundamental limitation.
> I disagree ...
This is not a topic open to debate, it is a statement of fact. I strongly recommend that you learn this topic, and the topics of mathematics and logic, where some statements can be proven true or false without ambiguity.
The Turing Halting Problem applies to all Turing-complete environments. The program under discussion meets the criterion. AI meets the criterion. Lean meets the criterion.
> There are certainly definitions of non-trivial ...
This is a logical fallacy known as "Logic Chopping" : https://iep.utm.edu/fallacy/#Logic%Chopping
> where this is still considered trivial, but I'm at a loss to what part of Turing's paper gives such a definition.
Yes, I can see that, but that's not what this discussion is about. Read this before posting again: https://en.wikipedia.org/wiki/Halting_problem
Dozens of online articles on this topic, make the same point in the same way. None of them digress into logical fallacies.
> This may be something we cannot come to an agreement on morally ...
"Morally", really? Another logical fallacy, another digression, and not the topic.
If you wish to say you have a counterclaim to the idea mistakes can be blocked regardless if every program can be proven to halt which is based in mathematical reasoning you must be able to state or produce the claim in the actual mathematical reasoning itself (or at least a link to the specific math directly relevant to the claim), not an English text summary of an entire paper/problem on Wikipedia. Anything less is not mathematical reasoning.
I'm unable to say more at this point as I can only assume you will continue to use that as a chance to quote and discuss everything but actual mathematics.
> If you wish to say you have a counterclaim to the idea mistakes can be blocked regardless if every program can be proven to halt which is based in mathematical reasoning you must be able to state or produce the claim in the actual mathematical reasoning itself ...
This is not a philosophy discussion, and Alan Turing already plowed this ground. The original claim "Bend - a language that blocks AI mistakes via proof [...]" is unsupportable.
> ... if every program can be proven to halt ...
But that's not so. You have introduced a qualifier that is known to be false.
> ... a chance to quote and discuss everything but actual mathematics.
Yes, I agree -- you should stop doing that. I keep referring to the original technical reason the original claim is unsupportable, others keep raising objections without trying to think through their positions.
It's not as though the Halting Problem is on the Millennium Prize Problem list, open to contradiction/reconsideration by some future challenge. It's a theorem, not a conjecture.
I've given notes of where in Turing's paper any type use triviality could be found, with direct page citations of the relevant original math, along with the mathematical reasons it doesn't have anything to do with the plain English statements you are making. This effort was a kindness done in good faith that I might find said mathematical definition of non-triviality for the halting problem somewhere in the paper, not something needed to show your claim devoid of a shown basis in mathematical reasoning so far. That much is apparent by the lack of a single mathematically defined claim specified by any of your messages.
That said, if you'd like me to formally show what e.g. the triviality in the rules of implication Turing was talking about are in a purely mathematical form I'd be glad to state with no English commentary out of good faith as well. This would seem a waste of time unless that's the part of the paper you think the definition of non-triviality can be sourced, but at least I'd at last have a clear mathematical claim from you to discuss.
It is now your opportunity to make a mathematical claim, of which proof by assertion this paper should apply because it proves something in general is not.
> That much is apparent by the lack of a single mathematically defined claim specified by any of your messages.
I posted the Turing Halting Problem Wikipedia page. It describes a theorem, not a conjecture that I need to prove, which shows the original poster's claim is contradicted by established facts.
Let me put it this way. If I say, "There are an infinity of primes," will you reply, saying, "I disagree"? That position would be equally appropriate -- that is to say, not appropriate at all.
Am I obliged to prove the infinity of primes by generating an infinity of candidate integers and prove that some of them are prime? No, and by the same token, I'm not obliged to reply to your naive demands and teach you why the Halting Problem falsifies the claim made by the original poster. That is not my responsibility, it is yours.
In mathematics, some things are conjectures -- the Millennium Challenge problems, for example. Others are theorems, meaning established truths, beyond dispute. Turing's Halting problem is a theorem.
Here is another authoritative reference to the fact I originally posted: "Did Turing prove the undecidability of the halting problem?" from the Oxford University Press -- https://academic.oup.com/logcom/article/36/1/exaf075/8417148 .
The question in the title is rhetorical, as you will discover if you read and understand the article I just linked.
> It is now your opportunity to make a mathematical claim, of which proof by assertion this paper should apply because it proves something in general is not.
How many more mathematical literature references will you require before you realize I have already met any burden of proof? I could post the entire technical proof here, but (a) the editors of this forum would kick me out, and (b) you would still refuse to accept the evidence.
How do I know this? Because you keep refusing to learn what you need to know to engage in this conversation.
There are an infinity of primes -- your turn.
The answer to what I'd say if this were about primes and a program which blocks outputting them in pure mathematics, despite there being infinitely many, would be (using a similar type of argument I gave early on for the current discussion):
(Apologies for the formatting, HN does not allow latex)
The thing blocking me from being able to do the same here is I defined a similarly styled argument about it being possible to construct a program (glad to give it in pure math if tou'd like) which blocks all non-halting programs by only allowing ones showable to be halting (n.b. much as the above example with primes, this result did not require listing every non-halting program and so does not disagree with the general halting problem) and you said Turing's paper contains some definition of non-triviality which says why that cannot be and then refuse to say what and where in this paper you believe this definition of non-triviality to be even though I could find no such thing.
If you said Euclid showed the above proof on primes does not apply because he gave some definition of non-triviality, telling me it's somewhere in his book Elements, and I said book IX proposition 20 does not say anything like that, so you say "it's on Wikipedia"... you could see why I have doubts you have any mathematical claim to produce defining said definition. At the very least, you could see how I'd still be awaiting to hear the actual mathematics you're using.
> The answer to what I'd say if this were about primes and a program which blocks outputting them in pure mathematics, despite there being infinitely many, would be ... [ snip ] ... Q.E.D.
Now I get it. I should have realized at the outset that this outcome lay in the future. You are here to pointlessly argue, not discuss nor debate.
> At the very least, you could see how I'd still be awaiting to hear the actual mathematics you're using.
Yes -- notwithstanding that I have posted links to that exact evidence from multiple sources. The problem is not a lack of evidence, the problem is that you refuse to read it.
On that topic, here is a link to Alan Turing's 1936 paper -- 36 pages long: https://www.cs.virginia.edu/~robins/Turing_Paper_1936.pdf
Andrew Wiles conclusively (dis)proved Fermat's Last Theorem. If you disagree, and since you have demonstrated a willingness to disagree with anything, I would have to post a link to the evidence, not the evidence itself, because the (dis)proof is 129 pages long.
As I post this, I'm trying to imagine the corpus of mathematical knowledge you're unwilling to accept, because it won't fit into a finite-sized Hacker News post -- relativity, both special and general, quantum mechanics, dozens of others.
I'm also trying to imagine someone whose literacy filter consists of "Tl;DR!"
It truly breaks my heart to see any of the math snipped out yet again. You sound more than capable of formulating your assertions in pure math but seemingly refuse to state it that way, which feels like watching a bright light in the world going out as it seeks to avoid rigor.
A set of theorems (of which I accept all you've named) without the definitions of exactly how and why they apply to the give problem is no more mathematics than a bunch of bricks is a chimney. I believe all of these beautiful proofs, I just don't believe you've properly demonstrated you can build your chimney with them. If you ever wish to build the chimney I'd be ecstatic, until then I think I don't think anything else can be said about how the pile of bricks aren't an example of one - especially if you're going to give the URL I already provided you when asking where the definition of the connection in it was https://news.ycombinator.com/item?id=49761146
I do wish you well and I'm sorry if my requirement for rigorous statements in math seems pointless to you. It's something I hold dear. I'll keep notifications in my script enabled in case you do want to start discussing the math rigorously, but I'll no longer try to convince you that's what's needed for your claims to hold mathematical weight anymore or any of the other things which seem to be bothering you for no gains.
> It truly breaks my heart to see any of the math snipped out yet again.
A false statement. I posted a link to the evidence, which cannot be summarized to satisfy your short attention span. Your unwillingness to read it only reveals your shallow grasp of modern technical topics.
Here is a short list of topics that cannot be converted into bumperstickers, your preferred medium of expression:
This list is by no means complete, but the last entry overlaps with the topic of this conversation, for reasons that will not be obvious to you unless and until you overcome your distaste for evidence.
> I do wish you well and I'm sorry if my requirement for rigorous statements in math seems pointless to you.
Excuse, me, what? I have posted links to the evidence that proves your position to be false, but you won't read it. You are to modern times what a religious fundamentalist is to science -- the primary obstacle to human progress.
Am I saying your unwillingness to absorb ideas outside your short attention span is itself an obstacle to human progress? No, actually, I'm saying you should avoid drawing conclusions without first examining the evidence.
It isn't only that you won't read the evidence that proves your position to be wrong -- that is simply sad, not fatal. It is that you draw conclusions without first examining the readily available evidence.
> A set of theorems (of which I accept all you've named) without the definitions of exactly how and why they apply to the give problem is no more mathematics than a bunch of bricks is a chimney.
Wow. You just dismissed the validity of all the topics in my list above, each of which produce everyday valid conclusions derived from very complex logical and mathematical antecedents.
Get professional help.
> A set of theorems (of which I accept all you've named) without the definitions of exactly how and why they apply to the give problem is no more mathematics than a bunch of bricks is a chimney.
A second reply. What you're not getting is that the mathematical equations in Turing's paper don't make its point. There are plenty of equations, but the paper's meaning lies in its logical arguments, for which the equations can only play a supporting role.
If the equations are taken out of the paper and presented separately, as you have repeatedly demanded, the paper's thesis falls apart. But to understand this, you would have to read the paper itself and absorb Turing's logical arguments. And the paper can't be made shorter without losing its meaning.
More evidence for this is given by the fact that Alonzo Church published a similar paper in 1936, different author, different equations, but the same logical argument and conclusion, such that Church and Turing are now given equal credit for the basic idea -- an idea that is supported by equations but not provided by them (https://courses.fit.cvut.cz/MI-VYC/church-a-note-on-the-ents...).
This is true in many parts of mathematics and logic. Another example is Einstein's 1905 paper later identified as the source of "special relativity". If you remove the equations and present them separately, all meaning is lost. In fact, in that case, the actual meaning of a particular equation was lost to Einstein himself, but that meaning occurred to his former math teacher Hermann Minkoswski, who went on to publish about something Minkowski called "spacetime". As before, the equations didn't convey the paper's real meaning, they could only play a supporting role. About this outcome Einstein later said, "Since the mathematicians have invaded relativity theory, I don't understand it myself any more."
Another more recent example is the recently solved "Navier–Stokes existence and smoothness problem" as it was titled by the Clay Mathematics Institute. The equation is easy to render, but as with the other examples, the problem to be solved goes far beyond the equation itself, and the meaning of the recent result lies not in the equation, but in its treatment and processing by AI.
In Navier-Stokes, everyone had access to the equations, but until recently no one could answer a fundamental question about it, and as with the prior examples, the real meaning requires one to read the articles that provide the logical reasoning. In each of these examples and many more, listing the equations can only be a preliminary step to true understanding.
More importantly, the meaning of the papers cannot be summarized in fewer words than are provided by the papers themselves. Mathematicians don't go out of their way to make their papers longer than their contents require, in fact, quite the opposite.
I can't believe you're still expecting bumperstickers to stand in for technical articles. As before, you should read the original articles instead of complaining that they're too long for your limited attention span.
> 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. No matter how much math is discussed, it'll never lead to anything if that's not where your understanding of the paper comes from.
It's one of the main things which separate hard sciences from things like Psychology where anyone can just talk about what they understand/see or want to link instead of define it in logic itself, and I must admit I've never believed much of the soft sciences because of that lack of rigor. Maybe that rejection of soft science as truth is a limitation of mine :) but I don't see myself abandoning the view any time soon.
>> 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.