7 ms·
In math, rigor is vital, but are digitized proofs taking it too far?
- ux266478 7mo agoRigor was never vital to mathematics. ZFC was explicitly pushed as the foundation for mathematics because Type Theory was too rigorous and demanding. I think that mathematicians are coming around to TT is a bit of funny irony lost on many. Now we just need to restore Logicism...
- moi2388 7mo agoRigor was always vital to mathematics. That it wasn’t vital to mathematicians is exactly why we need automated proofs.
- riverforest 7mo agoRigor is the whole point of math. The moment you start asking if there is too much of it you are solving a different problem.
- meroes 7mo agoIf rigor is the whole point why are we so focused on classical math (eg classical logic) not the wider plurality?
- SabrinaJewson 7mo agoHow does that relate at all? Classical logic is not any less rigorous than other kinds of logic.
- meroes 7mo agoBecause if rigor is all we cared about I’d think we’d spend more time on non-classical math.
- woopwoop 7mo agoRigor is not the whole point of math. Understanding is. Rigor is a tool for producing understanding. For a further articulation of this point, see https://arxiv.org/abs/math/9404236 https://arxiv.org/abs/math/9404236
- 1970-01-01 7mo agoThis conflates rigor with proof. Proof is the solve to the argument you are making. Rigor is how carefully and correctly the argument is made. You can understand something without rigor but you cannot prove it.
- layer8 7mo ago> You can understand something without rigor but you cannot prove it. I think I disagree. There are formal proofs and informal proofs, there are rigorous proofs and less rigorous proofs. Of course, a rigorous proof requires rigor, but that’s close to tautological. What makes a proof is that it convinces other people that the consequent is true. Rigor isn’t a necessary condition for that.
- storus 7mo agoRigor is one solution to mutual understanding Bourbaki came up with that in turn led to making math inaccessible to most humans as it now takes regular mathematicians over 40 years to get to the bleeding edge, often surpassing their brain's capacity to come up with revolutionary insights. It's like math was forced to run on assembly language despite there were more high-level languages available and more apt for the job.
- cbdumas 7mo ago> It's like math was forced to run on assembly language despite there were more high-level languages available and more apt for the job. I'm not a mathematician but that doesn't sound right to me. Most math I did in school is comprised concepts many many layers of abstraction away from its foundations. What did you mean by this?
- storus 7mo agoMy math classes were theorem, lemma, proof all day long, no conceptualization, no explanation; low-level formulas down to axioms. Sink or swim, figure it out on your own or fail.
- gzread 7mo agoIt seems you have never tried to prove anything using a proof assistant program. It will demand proofs for things like x<y && y<z => x<z and while it should have that built in for natural numbers, woe fall upon thee who defines a new data type.
- deleted 7mo ago[deleted]
- johnbender 7mo agoI’m confused by the calculus example and I’m hoping someone here can clarify why one can’t state the needed assumptions for roughed out theory that still need to be proven? That is, I’m curious if the critical concern the article is highlighting the requirement to “prove all assumptions before use” or instead the idea that sometimes we can’t even define the blind spots as assumptions in a theory before we use it?
- pavpanchekha 7mo agoIn calculus the core issue is that the concept of a "function" was undefined but generally understood to be something like what we'd call today an "expression" in a programming language. So, for example, "x^2 + 1" was widely agreed to be a function, but "if x < 0 then x else 0" was controversial. What's nice about the "function as expression" idea is that generally speaking these functions are continuous, analytic [1], etc and the set of such functions is closed under differentiation and integration [2]. There's a good chance that if you took AP Calculus you basically learned this definition. The formal definition of "function" is totally different! This is typically a big confusion in Calculus 2 or 3! Today, a function is defined as literally any input→output mapping, and the "rule" by which this mapping is defined is irrelevant. This definition is much worse for basic calculus—most mappings are not continuous or differentiable. But it has benefits for more advanced calculus; the initial application was Fourier series. And it is generally much easier to formalize because it is "canonical" in a certain sense, it doesn't depend on questions like "which exact expressions are allowed". This is exactly what the article is complaining about. The non-rigorous intuition preferred for basic calculus and the non-rigorous intuition required for more advanced calculus are different. If you formalize, you'll end up with one rigorous definition, which necessarily will have to incorporate a lot of complexity required for advanced calculus but confusing to beginners. Programming languages are like this too. Compare C and Python. Some things must be written in C, but most things can be more easily written in Python. If the whole development must be one language, the more basic code will suffer. In programming we fix this by developing software as assemblages of different programs written in different languages, but mechanisms for this kind of modularity in formal systems are still under-studied and, today, come with significant untrusted pieces or annoying boilerplate, so this solution isn't yet available. [1] Later it was discovered that in fact this set isn't analytic, but that wasn't known for a long time. [2] I am being imprecise; integrating and solving various differential equations often yields functions that are nice but aren't defined by combinations of named functions. The solution at the time was to name these new discovered functions.
- zitterbewegung 7mo agoI think the future of having lean as a tool is mathematicians using this or similar software and have it create a corresponding lean code. [1] This is an LLM that outputs Lean code given a mathematical paper. It can also reason within lean projects and enhance or fix lean code. [1] https://aristotle.harmonic.fun https://aristotle.harmonic.fun
- umutisik 7mo agoWith sufficient automation, there shouldn't really be a trade-off between rigor and anything else. The goal should be to automate as much as possible so that whatever well-defined useful thing can come out theory can come out faster and more easily. Formal proofs make sense as part of this goal.
- YetAnotherNick 7mo agoThe thing is if something is proved by checking million different cases automatically, it makes it hard to factor in learning for other proofs.
- storus 7mo agoThere are still many major oversimplifications in the core of math, making it weirdly corresponding with the real world. For example, if you want to model human reasoning you need to step away from binary logic that uses "weird" material implication that is a neat shortcut for math to allow its formalization but doesn't map well to reasoning. Then you might find out that e.g. medicine uses counterfactuals instead of material implication. Logics that tried to make implication more "reasonable" like relevance logic are too weak to allow formalization of math. So you either decide to treat material implication as correct (getting incompleteness theorem in the end), making you sound autistic among other humans, or you can't really do rigorous math.
- jojomodding 7mo agoPeople keep getting hung up on material implication but it can not understand why. It's more than an encoding hack--falsity (i.e. the atomic logical statement equivalent to 0=1) indicates that a particular case is unreachable and falsity elimination (aka "from falsity follows everything") expresses that you have reached such a case as part of the case distinctions happening in every proof. Or more poetically, "if my grandmother had wheels she would have been a bike[1]" is a folk wisdom precisely because it makes so much sense. 1: https://www.youtube.com/watch?v=A-RfHC91Ewc https://www.youtube.com/watch?v=A-RfHC91Ewc
- 7mo ago
- jl6 7mo agoImagine a future where proofs are discovered autonomously and proved rigorously by machines, and the work of the human mathematician becomes to articulate the most compelling motivations, the clearest explanations, and the most useful maps between intuitions, theorems, and applications. Mathematicians as illuminators and bards of their craft.
- tines 7mo agoBut in this future, why will “the most compelling motivations, the clearest explanations, and the most useful maps between intuitions, theorems, and applications” be necessary? Catering to hobbyists?
- layer8 7mo agoMapping theorems to applications is certainly necessary for mathematics to be useful.
- ndriscoll 7mo agoVery far in the future when AI runs everything, of course math will be a hobby (and it will be great! As a professional programmer I'm happy that I now have a research-level tutor/mentor for my math/physics hobby). In the nearer term, it seems apparent to me that people with stronger mental models of the world are able (without even trying!) to formulate better prompts and get better output from models. i.e. as long as people are asking the questions, they'll do better to have some idea of the nuance within the problem/solution spaces. Math can provide vocabulary to express such nuance.
- j45 7mo agoIs digitized proofs another way of saying the equivalent of a calculator, when a calculator was new?
- sxzygz 7mo agoThe problem with this ambition is that it turns mathematics into software development. There’s absolutely nothing wrong with this per se, however what happens is that, as in software, certain ideas get ossified. That’s why, for example, every OS has a POSIX layer even though technically the process/namespace/security model could be radically reimagined possibly to create more easily engineered, correct software. Mathematics is going through a huge, quiet, upheaval. The litmus test will be when, if ever, someone wins a Fields using a proof-assistant in an essential way.
- msteffen 7mo ago> what happens is that, as in software, certain ideas get ossified. That’s why, for example, every OS has a POSIX layer even though technically the process/namespace/security model could be radically reimagined possibly to create more easily engineered, correct software. Total amateur here, but it strikes me that one important difference is that performance matters in software in a way that it doesn’t in mathematics—that is, all proofs are equally valid modulo elegance. That means that abstractions in software are leaky in a way that abstractions in mathematics aren’t. In other words, in software, the same systems get reused in large part because they’ve been heavily refined, in terms of performance, unexpected corner-case behavior and performance pitfalls, documentation of the above, and general familiarity to and acceptance by the community. In math, if you lay new foundations, build some new abstraction, and prove that it’s at least as powerful to the old one, I’d think that you’d be “done” with replacing it. (Maybe downstream proofs would need some new import statements?) Is this not the case? Where are people getting stuck that they shouldn’t be?
- dooglius 7mo agoAgreed; e.g. if you prove something about the real numbers, the matter of how R is constructed out of your axiomatic system doesn't matter
- pas 7mo agothere are questions where the abstraction of real numbers becomes leaky, and some axioms (or their lack) poke through. https://en.wikipedia.org/wiki/Axiom_of_choice#Real_numbers https://en.wikipedia.org/wiki/Axiom_of_choice#Real_numbers
- pfdietz 7mo agoA few comments: (1) Math journals are being flooded with AI slop papers loaded with errors. I can see a time when they will require papers to be accompanied by formal proofs of the results. This will enable much of the slop to be filtered out. (2) Formalization enables AI to do extensive search while staying grounded. (3) Formalization of the historical math literature (about 3.5M papers) will allow all those results to become available for training and mining, to a greater extent that if they're just given as plain text input to LLMs.
- dbvn 7mo agoThere's no such thing as being too rigorous when you're talking about proofs in math. It either proves it or it doesn't. You get as rigorous as you need to
- anthk 7mo agoLLM's are not reproducible. Common Lisp, Coq and the like for sure are.
- WhitneyLand 7mo agoGreat quote from Hilbert, I think it’s also a useful thought for software development. “The edifice of science is not raised like a dwelling, in which the foundations are first firmly laid and only then one proceeds to construct and to enlarge the rooms,” the great mathematician David Hilbert wrote in 1905 (opens a new tab). Rather, scientists should first find “comfortable spaces to wander around and only subsequently, when signs appear here and there that the loose foundations are not able to sustain the expansion of the rooms, [should they] support and fortify them.”
- ratmice 7mo agoMy only complaint with the article is that it doesn't seem to mention that digitized proofs can contain gaps but that those gaps must be explicit like in lean the `sorry` function, or axioms.
- nicoburns 7mo agoYeah, I see a lot of people (especially on HN) bemoaning any science that isn't a controlled double blind experiment with a large sample size. But exploratory science is just as important as the science that proves things. Otherwise we wouldn't know which hypotheses are useful/interesting to test.
- harshreality 7mo agoAre they bemoaning that science is being done, or are they bemoaning that the experimental results have not yet reached high enough confidence to justify the conclusions being suggested?
- cap11235 7mo agoMore Doctors Smoke Camels!™
- JumpCrisscross 7mo ago> Are they bemoaning that science is being done The reflexive "in mice" comments seem to be bemoaning how science is done.
- casey2 7mo agoIn the long run creating a certificate that guarantees a certain probability of correctness will take much less energy. Right now we can run miller-rabin and show with 1-(1/10^100) certainty that the number is/isn't prime. Similar for hash collisions, after a certain point these can't happen in reality. If Anthropic can get their uptime from 1 9 to 9 9s (software isn't the bottleneck for 9 9s) then we don't need formally checked proofs.
- WCSTombs 7mo agoIt's easy to forget, as we all use digital tools in our day-to-day lives, that the world is fundamentally analog, and there's no way to escape that. Everyone trying to tell you otherwise is just selling snake oil, with one notable exception, which is mathematical rigor in proofs. It's understood now that a rigorous proof in math is exactly one that, in principle, can be digitized and checked automatically. Those are simply the same concept, so introducing a computer there is really a perfect fit of tool and purpose. If we can't use computers to automate the checking of mathematical proofs, then why have computers at all? It's the only serious thing people do that a computer can be literally perfect at! To be clear, there's much more to math than writing down and checking proofs. Some of the most important contributions to math have been simply figuring out the right questions to ask, and also figuring out the useful abstractions. Those are both firmly on the "analog" side of math, and they are every bit as important as writing the proofs. But to say that we have this huge body of rigorous argumentation in math, and then to finally do the work of checking it formally is "taking it too far," is a really bewildering take to me. No, I don't think formalizing proofs in Lean or other proof systems should dominate the practice of math, and no, I don't think every mathematician should have to write formal proofs. Is that really where we're heading, though? I highly doubt it. The article worries about monoculture. It's a legitimate concern, but probably less of one in math than in many other places, since in my experience math people are pretty independent thinkers, and I don't see that changing any time soon. Anyway, the conclusion from all this is that the improved ability for mathematicians to rely on automated tools to verify mathematical reasoning would be a great asset. In my opinion the outcomes of that eventuality would be overwhelmingly good.
- ralph84 7mo ago> that the world is fundamentally analog Isn't that still an unresolved question? Wave-particle duality and all that.
- WCSTombs 7mo agoI think there are some theories that the universe is fundamentally discrete at the lowest level below current capabilities of measurement, but to my knowledge none of those is widely accepted.
- emih 7mo agoI like the story in the article, but I think it tries to create some drama where there isn't any. I think it's great that a lot of work is done using proof assistants, because clearly it's working out for researchers; diversity of research and of methods is a great strength of science. I really can't see how you can "push it too far", pen-and-paper proofs are not going anywhere. And as more researchers write machine-checked proofs, new techniques for automating these proofs are invented (which is what my research is about hehe) which will only make it easier for more researchers to join in. > Currently, mathematicians are hoping to formalize all of mathematics using a proof assistant called Lean. _Some_ mathematicians are trying to formalize _some_ of mathematics using a proof assistant called Lean. It's not a new development, proof assistants have been used for decades. Lean 4 has definitely been gaining popularity recently compared to others, but other proof assistants are still very popular. > a dedicated group of Lean users is responsible for determining which definitions should go into Lean’s library The article makes it sound like there is a single, universal "The Lean Library" that everyone is restricted to. I assume it refers to mathlib? But at the end of the day it's just code and everyone is writing their own libraries, and they can make their own decisions.