8 ms·

> 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 Le

• markisus 3y ago
  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.
  • Tainnor 3y ago
    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.
    • markisus 3y ago
      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.
      • hgsgm 3y ago
        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.
        • Pazzaz 3y ago
          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.
• oulipo 3y ago
  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
• staunton 3y ago
  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.
  • hnfong 3y ago
    "Beyond reasonable doubt" is the level of proof required for incriminating somebody. Math generally has a higher bar (for better or worse..)
    • staunton 3y ago
      The way I would phrase it, the difference is in what kind of doubt is considered "reasonable".
• cscheid 3y ago
  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_Example_to_Type_Safety https://en.wikipedia.org/wiki/Value_restriction#A_Counter_Ex...).
  • markisus 3y ago
    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.
    • cscheid 3y ago
      > 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.
  • wk_end 3y ago
    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 https://github.com/coq/coq/issues/4294
• cvoss 3y ago
  > 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.
  • mcguire 3y ago
    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.
    • mcphage 3y ago
      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.
    • commonlisp94 3y ago
      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.
      • ukj 3y ago
• Ericson2314 3y ago
  Yeah any statement that goes back and forth a bit too fast between Lean and ChatGPT raises my suspicions.
• mcguire 3y ago
  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?
  • madsbuch 3y ago
    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.
    • hgsgm 3y ago
      Normal math also concisely cites pre-existing theorems
      • infogulch 3y ago
• User23 3y ago
  It’s unfortunate that semiotic has become a joke word. C.S. Peirce did seminal work tying it to logic.
• deleted 3y ago
  [deleted]
• TheOtherHobbes 3y ago
  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.
  • cscurmudgeon 3y ago
    > 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).
    • ukj 3y ago
      Sounds like you are on the path towards understanding that what we call “objectivity” is an inter-subjective construct.
      • cscurmudgeon 3y ago
        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.
• raincole 3y ago
  Compilers can have bugs. Hardware can have bugs too. Why are formal systems that run on a computer assumed to be bug-free?
  • staunton 3y ago
    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.
• hyperthesis 3y ago
  That particular quote isn't questioning Lean, but "convert[ing] the proof into inputs for Lean." GIGO
  • SkiFire13 3y ago
    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.
    • hyperthesis 3y ago
      You disagree then agree. Here's an elaboration of the point: https://news.ycombinator.com/item?id=37341439 https://news.ycombinator.com/item?id=37341439
• GoblinSlayer 3y ago
  >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.
  • dagw 3y ago
    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.
  • paldepind2 3y ago
    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 :)
• YeGoblynQueenne 3y ago
  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?
  • qsort 3y ago
    > 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.
• gopher_space 3y ago
  > 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.
• loglog 3y ago
  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.