Hacker News Reader

Comment by qsort | Hacker News Reader

> But is this foolproof? Is a proof a proof just because Lean agrees it’s one? In some ways, it’s as good as the people who convert the proof into inputs for Lean.

Having studied CS in school I'm sort of triggered by this. Might be the editorialization, but this is a statement I have a problem with.

I am not one of those who think that computers will save us all. My point of view is that computers are meaningless machines that do meaningless operations on meaningless symbols unless proven otherwise. This is what gets drilled in your head in any semi-decent CS program and it's a point of view I came to agree with completely.

But we have proven otherwise.

Proof checkers like Lean, Coq, Matita, Isabelle and the like are not like normal code, they are more similar to type-systems and code expressed in their formalisms is directly connected to a valid mathematical proof (see the Curry-Howard isomorphism).

They are usually constructed as a tiny, hand-proven core, and then built on their own formalism, ensuring that what is exposed to the end user is perfectly grounded.

If a program is accepted by the proof checker, then by construction it must be a valid mathematical proof.

Of course, computers are physical machines that can potentially make all sorts of mistakes. Hardware failures, cosmic rays, whatever. But the probability of that happening on a large scale is the same probability that seven billion people collectively hallucinated elementary theory and it's in fact not true that there are infinitely many prime numbers.

edit: Just a clarification: it's only this particular statement I have a problem with. The article is very much worth your time. Do not get derailed by the title, it's not some sort of "math is racist" nonsense.

View on HN

Once upon a time, the professor of a class on logic I was taking pointed out that, if you proved some famous open conjecture (I think Fermat's was the example) using some simple proof that everyone had just missed so far, mathematicians would pat you on the head, maybe give you an award or something, and you (and the conjecture) would become another forgotten footnote.

Major mathematical advances come from difficult problems when a new branch of mathematics is invented to solve them. Think of calculus, non-Euclidean geometry, and Turing machines (and their equivalents).

The problem I see with Coq, the proof checker I've worked with the most, and the others I've seen is that the proofs they result in are neither good, understandable programs nor good, understandable proofs. They are as complicated as complex programs, but written in something that isn't a half-way clean programming language, but they're also not written as a traditional proof. That goes back up to the article's point that the purpose of a proof is to convince and enlighten others.

Sure, I'd have to say a proposition proven in Coq is true, but how do you get from that to the ideas in the proof letting you go on to other problems?

I don't think the point is to either have good math or good code.

When you develop software in Coq and the likes, it is library code. It is high impact code that is guaranteed to be correct. It is written once and not maintained – You would never build the new Twitter in Coq.

When you develop math on Coq, you build abstractions. You just need to know that theorems that you are working on. Then you pull in all the lemmas in coq to help you solve that theorem. You do not need to understand the lammas coq uses to help you prove your theorem – coq does that for you. So your math is extremely concise. This is in opposition to normal math, where you need to be able to explain the hierarchy your theorem works on top of.

"It is written once and not maintained..."

Be careful, this is how you get the Ariane V first flight.

"You do not need to understand the lammas coq uses to help you prove your theorem..."

If I wanted to generalize your theorem or move it to some other base abstraction, the first thing I need to do is to read and understand your proof. If that proof is made up of Coq tactics chosen based on "whatever works", I'm going to have a bad day.

Now, many results especially in CS are made by reducing a new problem to an existing theorem, but I don't know how well that works as a general case.

Normal math also concisely cites pre-existing theorems

Ah but normal math is a social compact in a way that computer-aided proofs are not. Very few handwritten proofs are actually written down in detail, and there are various cases where attempting to do so actually failed or required new work to actually close the gap.

Proof assistants assist with normal math. They just make the normal formal and realiable.

I guess the hope is that eventually there will be a language which is roughly as easy to read/write as normal proofs in English but can be machine checked.

Lean comes closer than Coq, but is still far from this ideal. It may be that AI will need to be involved (as in, there could be a tactic that generates proof terms using an transformer or something).

> I guess the hope is that eventually there will be a language which is roughly as easy to read/write as normal proofs in English but can be machine checked.

That's what "declarative proofs" are for (as seen in Mizar, Isar, and formerly in the Coq plugin C-zar). Most proofs in interactive proof assistants are written as "proof scripts", which cannot be understood without playing them back in the proof assistant (in fact, specifically the version of the proof assistant that the "script" was originally written for) and checking how each step in the "script" relates to the current proof state.

Declarative proofs are more self-contained, in that the assumptions and conclusions involved in each proof step can be ascertained by just reading them in the code. They can also be naturally simplified into structural "proof sketches", where missing steps in the proof could potentially be filled by a proof-searching "AI".

> in fact, specifically the version of the proof assistant that the "script" was originally written for

Are Isar updates guaranteed not to break proofs?

Like Cobol?

Coqobol?

I think you'll get machines that can check human proofs first.

I think the only way to do this that anyone will find convincing is to have an LLM turn the human proof into a machine checkable one, so all the research into Lean etc. will still be useful.

There is something similar Nima Arkani-Hamed talks about Feynman equations during his amplituhedron lecture, pages and pages of equations being reduced to simple representation.

@56:26 in https://youtu.be/sv7Tvpbx3lc

Ironically, I consider the amplituhedron to be very unclear.

Every presentation by its author goes: "here's a triangle, here's a simplex, and now... ta-da... the amplituhedron is the same!"

He skips 15 steps every time. It's literally the "here's a circle, then another circle, and now just draw the rest of the owl", but in terms of theoretical physics.

He says in the lecture that physicists arrived at the simple representation by studying Feynman diagrams and looking at how terms cancel each other. And amplituhedron also gives rise to those same representation. This is the reason why he considers amplituhedron to be a good research path. He cites similar interpretation change that happened before in physics[0]

[0] : https://youtu.be/sv7Tvpbx3lc?t=2664

I think the quote is about the fallibility of the humans who convert theorems into statements of type theory. You could end up with a valid theorem, but not the theorem you meant to prove. This would be a bug in the statement of the theorem, not the proof.

For example, you might want to prove that a certain sorting algorithm is correct. You formalize the specification as "for every two integers i, j, output[i] <= output[j]" and prove that outputs of the algorithm satisfy this spec. However, this is not a correct characterization of sorting, since the algorithm might return the empty list.

1. Sure, but verifying a spec is still much easier than verifying a whole proof (as we traditionally do).

2. In that example that you gave, you would have additional evidence: if you use your system and every sort returns an empty list, you'd probably notice it quite quickly. You can also do manual or automated testing to see that it does the right thing for example inputs. If you then consider it to be unlikely that someone writes code that would exactly only work for example inputs and only satisfy the specification in the dumbest possible way, then you get some really good evidence that your algorithm is actually correct. 100% certainty is never possible, but there are still degrees.

Agreed. I think the interviewee is a little pessimistic when he says "I’m just not sure it’s any more secure than most things done by humans." about computer assistance. If the ABC conjecture were to be proven in Lean, I'm pretty sure it would be accepted as true by an overwhelming majority of the mathematical community.

The ABC conjecture "proof" is rejected because it uses definitions and arguments no one understands.

It would not necessarily be hard to program in those incoherent definitions and get them to prove a result. That wouldn't mean much.

This is different from just programming in the conjecture and letting Lean find a complete proof.

The proof is not rejected because people don't understand it, it's rejected because people don't think the proof is correct.

If the proof was translated to Lean, then it would mean a lot if it managed to prove the ABC conjecture because it would mean the proof was correct. It doesn't matter if the proof used crazy definitions. The statement of the ABC conjecture would still be understandable and so the ABC conjecture would be solved.

> The ABC conjecture "proof" is rejected because it uses definitions and arguments no one understands.

I would like to point out that it seems like the general consensus now is that Mochizuki's proof is incorrect.

And, as people pointed out early on, one of the problems with the Mochizuki paper is that it provides no new tools or results for other problems in the space. This is quite unusual and was a significant part of the skepticism about the proof being correct.

Contrast this to Wiles proof of the Taniyama-Shimura-Weil conjecture for semistable elliptic curves which proves Fermat's Last Theorem as a consequence and then led to a full proof which later became the "modularity theorem".

If Mochizuki used the tools from his paper come at something already proven from a different direction, that would have lent a lot more credence to his claims.

> 1. Sure, but verifying a spec is still much easier than verifying a whole proof (as we traditionally do).

I agree.

In the Metamath community, we also check all proofs with a collection of verifiers written by different people in different languages, all based on a very small kernel. That provides extremely high confidence in its correctness.

It's an important problem and people in formal verification are aware of it. One example of tackling this is that the Lean LTE team accompanies the proof with "several files corresponding to the main players in the statement" and "[they] should be (approximately) readable by mathematicians who have minimal experience with Lean [...] to make it easy for non-experts to look through the examples folder, then look through the concise final statement in challenge.lean, and be reasonably confident that the challenge was accomplished".

Details in this blog post: https://leanprover-community.github.io/blog/posts/lte-exampl...

I'm with you almost everywhere, but it's worth pondering this:

> If a program is accepted by the proof checker, then by construction it must be a valid mathematical proof.

I'd phrase it as "If a program is accepted by a _correct_ proof checker, then ...". That makes it clear that we can't escape having to consider how and why the proof checker is considered correct.

Edit: this is not entirely academic. from what I understand, the unsoundness of Hindley-Milner in the presence of polymorphic references was not immediately known (https://en.wikipedia.org/wiki/Value_restriction#A_Counter_Ex...).

To be ruthlessly, uselessly pedantic - after all, we're mathematicians - there's reasonable definitions of "academic" where logical unsoundness is still academic if it never interfered with the reasoning behind any proofs of interest ;)

But: so long as we're accepting that unsoundness in your checker or its underlying theory are intrinsically deal breakers, there's definitely a long history of this, perhaps somewhat more relevant than the HM example, since no proof checkers of note, AFAIK, have incorporated mutation into their type theory.

For one thing, the implementation can very easily have bugs. Coq itself certainly has had soundness bugs occasionally [0]. I'm sure Agda, Lean, Idris, etc. have too, but I've followed them less closely.

But even the underlying mathematics have been tricky. Girard's Paradox broke Martin-Löf's type theory, which is why in these dependently typed proof assistants you have to deal with the bizarre "Tower of Universes"; and Girard's Paradox is an analogue of Russell's Paradox which broke more naive set theories. And then Russell himself and his system of universal mathematics was very famously struck down by Gödel.

But we've definitely gotten it right this time...

[0] https://github.com/coq/coq/issues/4294

> there's reasonable definitions of "academic" where logical unsoundness is still academic if it never interfered with the reasoning behind any proofs of interest ;)

I wouldn't really so. If you were relying on the type system to tell you about any errors you made in your program, the revelation that your type system was unsound is not "only academic" simply because your program coincidentally didn't have errors. Just like it wouldn't be "only academic" if you discovered that your car's airbags weren't functional for the last 10 years even though you never had any accidents.

I'd also note that the correctness of the proof checker not only lies in the high level software code, but also the full stack of hardware down to the nanoscale.

Eg.

- Are you sure the compiler is correct?

- Are you sure the OS is behaving correctly?

- Are you sure the CPU isn't randomly glitching out?

There's a difference between believing that these things are correct 99.999% of the time, and claiming that it's mathematically proven to behaving correctly. Mathematical proof isn't statistics, so either you're willing to claim and defend the claim that the whole stack of the proof checker is correct, or you don't have a proof at all.

How one would prove that a physical modern CPU conforms to a formal spec I have no idea TBH. I presume the QA of chip manufacturers uses statistical methods.

> Are you sure the compiler is correct?

Use multiple different compilers and compare results

> Are you sure the OS is behaving correctly?

Use multiple different OSes and OS-versions

> Are you sure the CPU isn't randomly glitching out?

Use multiple different CPU types.

This is a great point. In a computer proof system, you produce judgements like "the term x has type is T", where the type "T" encodes the statement of a theorem and "x" is the proof. We must be certain that whenever the type checker verifies that "x has type T", it means that the theorem "T" is actually true. Such a meta-proof must be done on pen and paper, before any code is written at all. Any bug in this meta-proof would destroy our ability to rely on the computer proof system.

> Such a meta-proof must be done on pen and paper, before any code is written at all.

Not so fast; it could be done on a _different automated system_ (say, a smaller one) than the one you're building, in which case you're now relying on that system's correctness. Or it could even not be proven at all. This is not too different from what mathematicians do when they (often) say "assuming P != NP", or "assuming GRH", or "assuming FLT", etc etc. It's simply that it's worth being careful and precise.

> the same probability that seven billion people collectively hallucinated elementary theory

Just for fun, it's not unprecedented that the entire human race is disposed to mislearn basic truths about the universe which have to be unlearned when you get to the point where it matters. See quantum mechanics.

One hopes that conscientious mathematicians are careful to select axiomatizations (such as ZF set theory or the type system of Lean) which faithfully reflect reality. And, within such a system, we can be extremely confident in what we're doing. But the distinct possibility remains that the axiomatization doesn't actually match our universe and, say, admits a proof of false or implies something not physically realizable, such as that a certain computation should terminate, when no real life physical machine obeying the laws of physics can ever do so.

Be careful with things like "faithfully reflect reality". :-)

Euclidean geometry is intuitively good and seems to work on relatively small areas of the Earth's surface, but non-Euclidean geometries are inconsistent with it and more faithfully reflect a reality that lacks infinite flat planes.

This is not true.

They are incompatible sets of axioms, but they can describe the same set of shapes, although one system is going to be a lot more inconvenient than the other. The differences are logically interesting, but about as incompatible as choosing to make the origin of a euclidean system one corner of the room instead of another.

In contrast physical theories contradict each other by making different predictions which can be falsified.

At that level of pedantry even the halting problem is solvable. Just choose a suitable representation for the Turing machines in question.

Describe/represent the ones that halt using 1; and the ones that don’t halt using 0. This produces the pairs (TM1, 1), (TM2, 1), (TM3, 0) etc.

Using this encoding the problem becomes trivial. It’s all other encodings which are unwieldy, complex and inconvenient.

That's no longer the halting problem: formally, the input to a halting oracle is an index for some fixed choice of admissible numbering of the set of Turing machines, meaning one that can be computed from the standard numbering induced by some universal Turing machine. Your encoding is not admissible.

>That's no longer the halting problem

Just your luck. Under Univalence identity is equivalent to equivalence and it's computationally decidable.

So you should be able to produce a decider which determines whether any alternative encoding/representation is equivalent to the halting problem; or not.

Formally speaking Turing machines are formal language recognizers, so in which formal language is the formal statement of the Halting problem expressed in?

I'd also like to see the decider for "admissible" vs "inadmissible" encodings. Input validation is an Interesting problem-domain for sure.

(Of course, this is all for the sake of maximum pedantry)

> Just your luck. Under Univalence identity is equivalent to equivalence and it's computationally decidable. So you should be able to produce a decider which determines whether any alternative encoding/representation is equivalent to the halting problem; or not.

Moving to a constructive setting lets you say things like "all functions are computable" because it has a restricted notion of function. It does not give you any new information about classical objects.

You say “restricted” I say “better defined”. Either way - A constructive setting is more expressive.

So express your English adjectives in Mathematics.

What do you mean by “restricted” when you are characterising a function?

Show me the decider… for “classical” and “non-classical” objects.

That is the definition of information; is it not? The answer to a yes/no questions

Is the object classical? Yes/no.

> You say “restricted” I say “better defined”.

Sure, whatever - the point is that they're different objects, and results about one are not results about the other.

> What do you mean by “restricted” when you are characterising a function?

I mean whatever the word "function" means in a given setting. A classical function X -> Y is a relation such that if `(x, y1)` and `(x, y2)` hold then `y1 = y2`. A function in intuitionistic type theory is a well-typed lambda term. A function in the categorical semantics of a type theory is an exponential object. And so on.

> Show me the decider… for “classical” and “non-classical” objects.

No such thing: it's a metatheoretical judgement, not a theorem. Same story as type errors: within the language, `stringToUpperCase (5 :: Int) :: String` isn't a false statement, it's just inexpressible nonsense. There is no such object as `stringToUpperCase 5` and so nothing can be said about it internally. When we talk about it, we're talking, from outside the language, about a syntactic construct.

> That is the definition of information; is it not? The answer to a yes/no questions

No. Self-information of a given outcome with respect to a random variable, which is probably the most common sense of the word, is the negative log of its probability. Shannon entropy, also often called information, is the expected self-information of a random variable. Mutual information is the KL divergence of a joint distribution and the product of the respective marginals. There are other notions.

>Sure, whatever - the point is that they're different objects, and results about one are not results about the other.

Sorry, I don't understand what you mean by "same" and "different".

By "same" do you mean =(x,y). And by "different" do you mean ¬=(x,y)

Or do you mean something like same(x,y) = { 1 if ??? else 0 }

>A classical function X -> Y is a relation such that if `(x, y1)` and `(x, y2)` hold then `y1 = y2

You seem to be confusing syntax and semantics here, and the infix notation isn't helping...

What does =(y1, y2) mean? What does =(x,x) mean?

>No such thing: it's a metatheoretical judgement, not a theorem.

What do you mean? Judgments are first-class citizens in Univalent Mathematics. a:R is a judgment that object a is of type R. This literally means "a proves R", and the particular expression "first class citizen" has well-understood meaning in Programming Language design ( https://en.wikipedia.org/wiki/First-class_citizen ).

>`stringToUpperCase (5 :: Int) :: String` isn't a false statement, it's just inexpressible nonsense.

So I must be a miracle worker then? Expressing the inexpressible nonsense...

   In [1]: def stringToUpperCase(x): return(str(x).upper())
   In [2]: stringToUpperCase(int(5))
   Out[2]: '5'

>No. Self-information of a given outcome with respect to a random variable, which is probably the most common sense of the word.

Speaking of randomness in a classical setting, this function exists, right?

f(x) = { 1 if random(x), else 0 }

No, the comment above mine is the one being pedantic. We can absolutely talk about physical correspondence of mathematical concepts, even though there are multiple equally good logical systems for describing them.

Correspondence is a relation.

Relations are functions.

Can you tell us more about this function which relates Mathematical concepts to physical reality?

> Relations are functions.

That is how they are defined in set theory based math. The mathematical definition is not the only meaning of a word. When when start to talk about the physical world, we need additional concepts. You are welcome to read the wikipedia page about correspondence theories of truth.

The fact is you are talking about the meaning of words. Be they English words; or Mathematical words.

If you are going to talk about the correspondence theory in the same breath as you are talking about any language - you need to solve the symbol-grounding problem.

What function/mechanism/relation (or if you don't like any of those words - pick your own) grounds symbols?

https://en.wikipedia.org/wiki/Symbol_grounding_problem

What is the sum of the interior angles of a triangle?

Let's recall your original comment. You said we can't talk about reality correspondence of math because multiple logical systems can describe physical space equally well.

A triangle in a euclidean system is not the same shape as a triangle in spherical, etc. They are only equivalent in that they have an analogous logical definition in their separate systems.

They don't look the same. They don't describe the same physical phenonoma either. In other words, the physical correspondence is not the same, so there is no contradiction.

What? I said nothing of the sort.

In what we laughingly call "normal" geometry, given a line L and a point P not on L, there is exactly one line L' through P parallel to L. In this case, the interior angles of a triangle sum to 180 degrees.

In hyperbolic geometry, there is more than one line L', L'', etc., through P that are parallel to L. In this case, the interior angles of a triangle sum to <180 degrees.

In elliptic geometry, there are no lines L' through P parallel to L. (You also have to alter Euclid's 2nd axiom, defining a line as extending indefinitely.) And in this case, the interior angles of a triangle sum to >180 degrees.

Triangles are triangles; they have three points and three line segments. Their properties, however, are inconsistent in the three axiomatic systems.

If you are operating in a relatively small area, say a bronze-age farmer's field, Euclid's axioms satisfy all your geometrizing needs. If, however, you are on the somewhat-spherical Earth and are dealing with a large enough area, you can make a triangle with three 90 degree interior angles. You can tell which geometry your "physical space" is dealing with, and if you use the wrong one then you will get wrong answers.

For more than 2000 years, geometers assumed their space was essentially Euclidian. It turns out that is not really true, and it also turns out that there are (now, common) situations where the difference matters. So when you do any applied math, you assert that your axioms "faithfully reflect reality". And you may be wrong. And you may not have any way of knowing you are wrong. And you may not even have the mathematical tools to know what "wrong" means.

> Be careful with things like "faithfully reflect reality". :-)

Let's be careful with our terms!

There is the universe, and then there's reality. They are not the same thing, they only seem that way because that is the model everyone's been raised on, and that "fact" is reinforced and defended daily.

Or even Newtonian Physics, which faithfully reflects reality—as long as you're not too large, or you're not traveling too fast. And then it starts to break down.

I think his argument is exactly that, those formal systems can suffer from errors (even though they've been checked), because the compiler could have errors, the processor could have errors, etc

So in the end, it's always a question of "community" and "belief that things seen by sufficiently many people are right", eg that after 10 years of using a CPU, we've identified and fixed most bugs, and so the program is even more likely to be valid

You're still performing meaningless operations on meaningless symbols. All you've done is picked a subset that looks - to you - as if it's a little less meaningless.

It's a problem of epistemology, not logic.

Logic itself is subjective. We have a set of heuristics we use to decide if something is "true" in a mathematical and scientific sense. But fundamentally they rely on concepts like "truth" and "logic" which we experience subjectively.

We label a certain set of psychological experiences "true", a certain related set "logical", and a different related set "experimentally valid."

But all we really have is a set of experiences that are subjectively consistent (more or less) and shared.

IMO it's quite likely we're missing a lot. Far from having god-like insight into the ultimate nature of truth and reality our minds are actually quite small and limited.

Many relationships, operations, and elements of objective reality are literally invisible to us because they're far too complex for us to imagine, never mind experience and understand.

This matters because potentially AI may not have the same limitations. We're just getting started with associative cognitive modelling based on ML data compression as opposed to mechanical machine building - which is what traditional code is.

That's a fundamental difference of approach, with the potential to work with a much larger conceptual and symbolic space than we're capable of.

I suspect we'll see some quite interesting outcomes.

> Logic itself is subjective. We have a set of heuristics we use to decide if something is "true" in a mathematical and scientific sense. But fundamentally they rely on concepts like "truth" and "logic" which we experience subjectively.

I agree that it is this way, but does it have to be? Is it physically necessary to perceive defection from this dilemma as "pedantic" (see below, how surprising!), or might it only be culturally necessary?

Take your claim for example: you are not distinguishing between logic itself and our experience of logic. You are objectively correct that there is in fact no distinction on one level (experience), but that is not the only level that exists.

How are questions of this nature (essentially: existence) answered in the physical realm, where we have high levels of skill and experience?

> Logic itself is subjective

Not really, by your logic (heh) everything is subjective: including your own argument about logic being subjective (which in turn uses logic).

This problem is why I strongly dislike social relativism arguments. It's sloppy reasoning and I can't make heads or tails of what they're asserting. I also disagree with the interviewee for this reason, I think his argument is also sloppy, he is conflating two different issues.

(One would think I'm some kind of conservative; I'm a gay, Asian American leftist who happens to have a STEM background, and so I hate reading about "socially constructed" arguments--which is what this article is a variation of.)

OK, so you dislike relativistic arguments.

Relative to which objective standard for reasoning are you asserting that any given argument is "sloppy"?

It's a turning point in one's life when we come to acknowle that we don't have to like the fact that relativism is true.

For literal centuries we have known absolute epistemological relativism is childishly easy to self refute.

Maybe (spot the computational/monadic joke).

In what objective system for evaluating proofs will you be presenting this “refutation”?

This whole “we have known” smells of a bandwagon fallacy already. Who do you represent?

I find it mildly ironic that I have to explain evaluation (and it’s dependency on a meta theory) on a forum full of computer scientists…

Let’s think in nano baby steps:

A. In what system are you presenting your argument here in your comment? Is that system objective or subjective.

B. If subjective, then I declare your argument to be false for me. End of story.

C. If objective, then congrats, you refuted yourself.

I find it wildly ironic that you condescend and resort to veiled ad hominem on top of a Logic/Philo 101 fallacy known for literal centuries.

Also, the statement “there is an objective system X” doesn’t imply “we fully know the system X”

I represent scientists and logicians and philosophers that have known this for, once again, centuries. People call X background or classical logic.

https://plato.stanford.edu/entries/logic-classical/

A. I am not presenting arguments. Only observations and inferences based on my understanding on the evidence.

B. If you declare my “argument” subjective (and therefore false for you, but true for me) you agree with my overall claim Q.E.D

C. Is it this one then? How would you prove this?

D. It is mighty presumptuous of you to assume that I subscribe to classical logic; or even a consistent logic for that matter. Or that I subscribe to the same logic at different times of day.

E. I am not impressed neither by your religion; nor by the writings of your prophets. Nullius in verba

> I am not presenting arguments. Only observations and inferences based on my understanding on the evidence.

That is what counts as an argument! An argument is a technical term from logic and includes inferences and observations (observations are single step inferences). My bad on using logic jargon, but yes, inferences/arguments/proofs all apply here. So what system are you presenting this inference in? Is that objective or subjective?

> B. If you declare my “argument” subjective (and therefore false for you, but true for me) you agree with my overall claim Q.E.D.

No, the real beauty of subjectivity is that it allows me to disagree at any level. And I disagree with you on your point above, invoking the full power of subjectivity.

In fact, let me do 100% subjectivity on the whole set of comments here, and declare all your statements false for me.

(Also, the above is proof by cases. And step B/C's conclusions alone don't go out to the outer level alone as you seem to assume. You have to combine them both).

Now, I should be getting paid for doing a logic 101 in the comments ;)

You can’t tell if my inferences are objective or subjective? Why does the distinction even matter then?

The more of my comments you declare false - the more evidence you are providing in support of relativism. It is a peculiar way to agree to my point (via disagreement).

Is that what you call “logic”?

It looked like you were making up the interpretation as you go along…

Sounds like you are on the path towards understanding that what we call “objectivity” is an inter-subjective construct.

I know you are being sarcastic, but this isn't a strange concept and this something philosophers have known for generations.

Let us say you claim "Nothing is objective". Then it doesn't take a genius to assert that your claim "Nothing is objective" isn't objective.

I have no idea what your metric for "strangeness" is.

Using similar reasoning we can also assert that "The speed of light is objective" is not an objective claim.

And we can further assert that both the inner and outer statements are true without arriving at a contradiction.

It doesn't take a genius, merely a very thick skin and a grasp of contextuality, to hold this perfectly reasonable conclusion in a society dominated by naive understanding of non-contradiction.

Objectivity, being an unattainable philosophical ideal, it doesn't prevent us from using the term in more pragmatic/cultural/inter-subjective sense. A white lie - if you will - that only a determined pedant would scrutinize to such philosophical extent.

Just as well, such overt pedantry deserves mockery and contempt.

Logic is subjective because it takes a lot of focused effort to align it with reality.

Here we go in circles. Is your statement about logic subjective or objective? Do you use logic to arrive at that conclusion?

The thing that these systems offer is "having to check less code". In some situations, that's huge. In others, it's not worth the effort it takes to get there and maybe doesn't actually reduce the complexity of checking that it all makes sense.

In other words, maybe you proved something beyond reasonable doubt, but that's completely useless if you misunderstand what it was that you proved.

"Beyond reasonable doubt" is the level of proof required for incriminating somebody.

Math generally has a higher bar (for better or worse..)

The way I would phrase it, the difference is in what kind of doubt is considered "reasonable".

For me, the entire article can be summarised in the following quote from it:

>> So there’s a big mess. We are limited in what we can do.

We are limited in what can do. All our formal systems are flawed. That's including arithmetic and Gödel proved that any system powerful enough to represent arithmetic will always be flawed. The machines we have that compute our formal systems with us -and it never stops doing my head in that it's possible to create physical machines to calculate what exists only in our thoughts- our computers, they are flawed, too, because they are based on the same flawed formal systems, the same limitations as ours. We cannot use such machines to escape their own, our own, limitations.

>> But we have proven otherwise.

Have we now. To whom?

> We are limited in what can do.

It's not wrong that we are limited in what we can do, but we are limited in the same sense a Turing machine is limited by the halting problem. We are limited in a very specific and precise sense.

> All our formal systems are flawed.

This threads dangerously close to the pop-culture take that math is flawed. I can accept this statement only if we take 'flawed' to mean 'incomplete' in the Godel sense. We don't say that integers are flawed because they aren't a field, that's how integers work. We should avoid needlessly loaded words.

> Have we now. To whom?

We don't prove things to someone. Proofs just are.

There's a sleight of hand at play here. A proof in the technical sense (let's call them Tproofs), as a series of deductions, is a mathematical object, not unlike the number five. A proof in the common sense (let's call them Cproofs) is an informal argument to convince other human beings that there exists a Tproof with certain characteristics. In this sense it's easy to see how Cproofs are social phenomena. They are basically ways to communicate with other human beings. Not unlike how banks create money when they issue loans, backed by nothing by the community's trust, a mathematician can write a Cproof standing for a Tproof, backed by the trust of his colleagues. Mathematics could not meaningfully function without this socially constructed web of trust, exactly like the economy could not function if our only mean of exchange were physical coins.

I have no problems in accepting that, in this sense, mathematics is a community effort and is strictly dependent on such community existing.

But there lies my argument. A proof-checker accepting a proof offers a very strong guarantee that an equivlent Tproof exists, stronger than any number of peer-reviewers could offer.

Therefore, to the extent that we deem epistemologically possible to mathematically prove a statement, a proof being accepted by a proof-checker is a mathematical proof.

The radical skeptic's argument that it's not, in fact, possible to mathematically prove statements in any meaningful sense is as always both perfectly irrefutable and perfectly uninteresting.

>> We don't prove things to someone. Proofs just are.

I think you need to do a bit of reading, to see what others have said on this subject, because you seem convinced you have the right attitude and the right frame of mind- but you only manage to trip yourself into making absurd statements like the one above. Proofs just are? Where?

I suggest you start here:

https://www.cs.umd.edu/~gasarch/BLOGPAPERS/social.pdf

And here, for a bit more context:

https://m-cacm.acm.org/magazines/2021/7/253448-program-verif...

Program verification, while interesting in its own regard, has nothing to do with what we're talking about here.

Proofs as studied by mathematical logic are mathematical objects, not something you "prove to someone", that's the entire and only point, and it's extremely well-grounded in existing theory. It's not even a contentious point, it's not something reasonable people can disagree on.

>> Proofs as studied by mathematical logic are mathematical objects, not something you "prove to someone", that's the entire and only point, and it's extremely well-grounded in existing theory.

Which theory is that? You're saying there's some theorem that proofs are mathematical objects that "just are"? What theorem is that? Can you point to it?

A tree of derivations is a mathematical object that formally represents a proof, which is connected to the way programs are written in proof checkers via the Curry-Howard isomorphism.

When we say "proof" in logic we mean that.

In common parlance, a "proof" is instead an informal argument.

I know that you know that, because I read your messages before and I know you are not an idiot. You are just dwelling on a rhetorical flourish for no particular reason.

I can't say whether I'm an idiot or not but, indeed, my background is in logic programming, first order logic and automated theorem proving (and other fields, not related to our discussion). Thus, I know that there is no formal concept of "proof" in logic. Even in automated theorem proving we formally define derivations, or deductions (which can be represented by the "mathematical objects" in your comment), but not proofs. As far as I know there is no mathematical or computational procedure that can construct "a proof", only arrive at a result that can be considered a proof, when the result is inspected by a human mathematician or computer scientist.

The concept of "proof" is, to my knowledge, only an informal concept, that only makes sense, and is only communicated, between humans. In mathematics that is even more so than in computer science. Certainly I wouldn't expect any expert on logic and proofs, to say that proofs "Just are". That sounds mystical, practically Platonic.

To give a concrete example (and you will excuse, I hope, my penchant for rhetorical flourishes, or at least terminological clarity, when I speak of the matters of my expertise) in Resolution-based automated theorem proving the derivation of the empty clause during a Resolution-refutation of a goal clause can be considered as a proof-by-refutation of the complement of the initial goal. That is so because we know that, if a set of clauses, Π, is unsatisfiable, then the empty clause is a logical consequence of Π. Therefore, if we can derive the empty clause from the union of a goal, G, and a set of clauses, Σ, we can assume that G is false, with respect to Σ (or, more precisely, that G is not a logical consequence of Σ) and that, therefore, ¬G must be true. We can do all that because we have fuzzy, human-readable proofs that convince us of the relation between Σ and G, and the derivation of the empty clause from their union; for example, in the Resolution theorem by J. Alan Robinson [1]. It would not be possible to set up an automated theorem proving system without such a human-readable, and human-convincing proof. Because nobody would trust it.

In fact, the Resolution Theorem, essentially a statement of the soundness of Resolution, is a statement of such irrefutable simplicity that there can be no doubt of its truth and, as far as I know, it has only been proven once, by Robinson, then his proof cited by anyone else interested in the matter. The completeness of Resolution on the other hand is more complicated to show and there have been many different proofs of it, in different forms (i.e. the Refutation-completenss of Resolution, and the Subsumption Theorem, proved by Robinson and others in different ways). Given that there are now many different proofs of the Completeness of Resolution, arriving at it from different directions, we can also be reasonably secure in the knowledge that Resolution is complete. We may still be wrong. Some proofs have been shown to be wrong [2].

That is how proofs work in practice.

I commented to help you understand where you are wrong, and because I, in turn, was "triggered" by your arrogant insistence about things you clearly do not know as well as you think you do. I suggested you do a bit of reading to avoid polluting our common space on HN with bullish ignorance. You reacted with offense. That is a natural reaction, and I have experienced it myself, but I hope that you can nevertheless take something useful from our exchange. I have studied long and hard to acquire the knowledge that I have and I consider it my responsibility to share this knowledge. Perhaps I should refrain from doing that in the future though, if it ends up being more "triggering" than informative.

________________________

[1] A machine-oriented logic based on the Resolution principle, J. A. Robinson, journal of the ACM, Jan. 1965.

https://dl.acm.org/doi/10.1145/321250.321253

A text that I recommend to anyone intersted in automated theorem proving, and proofs in general.

[2] https://homepages.cwi.nl/~rdewolf/publ/ilp/ilp95.pdf

You say your intent is to teach and to inform.

I don't doubt that this is the case. The reason why I found your response triggering is that you did not come off, in this exchange, as genuinely having that intention, from the very beginning.

To be completely frank it just looked as though you were looking for a fight.

I recognized your username among the responses. I knew you had that kind of background and wanted to hear from you.

I am not an expert nor I claim to be, mine are just fade memories, but as far as I know using "proof" to mean "derivation" is not uncommon, see for instance[1][2][3]. I was very particular about separating the "formal" and "informal" kind in any case. I don't think I can be accused of playing fast and loose with definitions.

If you are trying to correct me on something else, I don't understand what it is.

Since you brought up that point yet again, by "proofs just are", an unfortunate choice of words, I do not mean anything mystical or platonic. I never had any intention of making such claims and I certainly don't stand by anything like it. I wanted to say that derivations (I used the "proof-in-the-formal-sense" language to which you object, I am amending it here) are mathematical objects, proofs (meant as you do, informally) are social processes.

I do not understand your response as saying anything different.

As far as I understand, all you're objecting to is my use of language. This is perhaps fair, but not terribly interesting. If there's something else, I'm afraid I failed to understand what it is.

In any case, thank you for this exchange.

I would like to encourage you to keep sharing your knowledge if you can make the time. I am sure this common space would benefit from it.

---

[1] https://www.ams.org/notices/200811/tx081101395p.pdf [2] https://link.springer.com/referenceworkentry/10.1007/978-3-0... [3] https://monks.scranton.edu/files/courses/Math299/math-299-le...

Thank you for your kind comment and for your patience. I think my comments above were awkward and didn't quite get my point across, and that's obviously not your fault but mine. Hopefully we'll have the time to discuss this issue again in the future. I'm sorry that we started off on the wrong foot.

> The radical skeptic's argument that it's not, in fact, possible to mathematically prove statements in any meaningful sense is as always both perfectly irrefutable and perfectly uninteresting.

Interesting to me is whether this "the" "radical skeptic" you're mocking is as it seems to be. I'd say it has the odor of a very convenient rhetorical strawman.

When practicing logic, don't forget the importance of ontology, as one could learn from epistemology. But then, that's a lot of work, and that sort of thinking "is" "pedantic".

Welcome to Planet Earth, circa 2023, {the culture you live in}, please enjoy your stay.

> But the probability of that happening on a large scale is the same probability that seven billion people collectively hallucinated elementary theory and it's in fact not true that there are infinitely many prime numbers.

That's the fundamental problem. We're building the machines to verify an internally consistent idea that we're all pretty pleased with. For example, type systems don't tell you that your data is true or correct, they just provide a framework of assumptions to work from that turn out to be really useful. Each type system will provide a different view on your data/process/etc.

Most senior, non-applied mathematicians in academia (including those with fancy titles at prestigious universities) outright refuse to adapt even simplest technological advances, like version control, let alone think about possible large scale transformation of mathematics. I wouldn't take take anything that they say about technology too seriously.

That particular quote isn't questioning Lean, but "convert[ing] the proof into inputs for Lean." GIGO

That's not how it works. If you input garbage in Lean or other proof checker they will just tell you it's wrong. You would have to input garbage in the statement you want to prove for them to accept a wrong proof (which must still be correct for that garbage statement!). To rule this out you just have to manually check the translation of the statement, which is most often much much smaller than the proof itself.

You disagree then agree.

Here's an elaboration of the point: https://news.ycombinator.com/item?id=37341439

>If a program is accepted by the proof checker, then by construction it must be a valid mathematical proof.

Huh? How? Truth is an empirical fact, you can't possibly define it into existence.

You have a point, but to be fair the person you replied to didn't use the word "truth". They said "valid mathematical proof". An in the context of type theory or formal logic "valid proof" is indeed something that has been "defined into existence" (in type theory "valid proof" ≈ "well-typed term"). Whether it represents "truth" is a different matter. Though such systems can (ideally) be proven sound in and with respect to "normal" mathematics. At that point I guess the "truth"ness depends on you overall belief in math :)

All mathematical "truths" are defined into existence as you call it. All mathematical proofs are essentially of the form If A Then B. B is only a "truth" since we defined A a certain way and accept it as True. Due to its very nature, there are no empirical facts in mathematics.

You can argue that the is no Truth is mathematics, which is a perfectly reasonable position to take.

Yeah any statement that goes back and forth a bit too fast between Lean and ChatGPT raises my suspicions.

It’s unfortunate that semiotic has become a joke word. C.S. Peirce did seminal work tying it to logic.

Compilers can have bugs. Hardware can have bugs too. Why are formal systems that run on a computer assumed to be bug-free?

They aren't assumed to be bug-free. It's simply known that the vast majority of bugs that occur in practice and that you have to care about aren't compiler or hardware bugs. So formal systems have a lot less bugs.

Reply on news.ycombinator.com