The issue is when people conflate formalism with truth itself. I know a lot of people who reject anything that isn't under the umbrella of "stuff that is formalised", even if it can be formalised but was simply not presented as formalised in its first incarnation.
Why formalize mathematics – more than catching errors
71–80 of 80 posts
Re: Why formalize mathematics – more than catching errors
#72Earlier quoted context omitted.
For mathematics and certain fields, that is true. But the formalism matters, and as some have argued, the Fregean style that came to dominate in the 20th century is ill-suited for some fields, like linguistics. One argument is that linguists using this style inevitably recast natural language in the image of the formalism. (The traditional logical tradition is better suited, as its point of departure is the grammar o…
> And it is always important to make a distinction between the abstractions proper to the formalism and the object of study. A common fallacy involves reifying those abstractions into objects of the theory, at least implicitly. I agree 100% and feel like I have seen a lot of people in physics kind of fall into this trap. The model is not the thing itself.
Are you sure you are really talking about Physics? Are you talking about actual research in physics, or physicists applying their way of thinking in other things?
Re: Why formalize mathematics – more than catching errors
#73Earlier quoted context omitted.
Bessis [1] argues that formalism - or loosely math writing - is foundational to clarifying intuition/meaning in a way that natural language cannot. Imagine it as a scalpel carving out precise shapes from the blur of images we carry thereby allowing us to "see" things we otherwise cannot. I am curious to try out lean to understand how definitions in lean are able to operationally capture meaning in an unambiguous mann…
It is interesting that you argue for formalism using a metaphor in natural language, rather than use a mathematical/data oriented argument. I find the metaphor pleasing in a way that I suspect a more data driven argument would not be.
Right tool for the job. Just like formalism is for math.
Re: Why formalize mathematics – more than catching errors
#74I have proven quite a few theorems in Lean (and other provers) in my life, and the unfortunate reality is that for any non-trivial math, I still have to figure out the proof on paper first, and can only then write it in Lean. When I try to figure out the proof in Lean, I always get bogged down in details and loose sight of the bigger picture. Maybe better tactics will help. I'm not sure.
> Maybe better tactics will help. I'm not sure. I don't see why they would. If anyone is curious about the phenomenon, the second problem in session 7 at https://incredible.pm/ [ ∀x.(r(x)→⊥)→r(f(x)) ⟹ ∃x.r(x)∧r(f(f(x))) ] is one where the proof is straightforward, but you're unlikely to get to it by just fooling around in the prover.
In principle, LLMs can do this already. If you ask Claude to express this in simple words, you will get this translation of the theorem:
"If applying f to things makes them red whenever they're not already red, then there must exist something that is red AND stays red after applying f twice to it."
You will be able to interact like this, instead of using tactics.
Re: Why formalize mathematics – more than catching errors
#75Earlier quoted context omitted.
> Maybe better tactics will help. I'm not sure. I don't see why they would. If anyone is curious about the phenomenon, the second problem in session 7 at https://incredible.pm/ [ ∀x.(r(x)→⊥)→r(f(x)) ⟹ ∃x.r(x)∧r(f(f(x))) ] is one where the proof is straightforward, but you're unlikely to get to it by just fooling around in the prover.
In principle, LLMs can do this already. If you ask Claude to express this in simple words, you will get this translation of the theorem: "If applying f to things makes them red whenever they're not already red, then there must exist something that is red AND stays red after applying f twice to it." Now the proof is easy to see, because it is the first thing you would try, and it works: If you have a red thing x, then…
For anyone else for whom the justification for “either x and f(f(x)) are both red, or f(x) and f(f(f(x)) are both red” was not immediately obvious:
H: ∀x.(r(x)→⊥)→r(f(x))
goal: ∃x.r(x)∧r(f(f(x)))
If f(f(x)) is red:
x is a solution (QED).
f(f(x)) not being red means f(x) must have been (by contraposition of H) and that f(f(f(x))) will be (by H); therefore, f(x) is a solution.Re: Why formalize mathematics – more than catching errors
#76Not super convinced by this analogy. Tooling and convenience feel secondary in math. If formalization doesn't help us do better mathematics, not just more structured mathematics, I'm pretty skeptical these benefits will justify the cost.
Re: Why formalize mathematics – more than catching errors
#77Noob question here. Say I'm wanting to formalize a proof. How do I know that what I'm writing is actually a correct formulation? If it gets more complicated, this problem gets worse. How do I know the thing it is checking is actually what I thought it was supposed to check? I guess this is a bit like when you write a program and you want to know if it's correct, so you write some tests. But often you realize your tes…
A point that is maybe not obvious to people who have not done mathematics at a high level or done “new” mathematics, is that often you end of changing your theorem or at least lemmas and definitions while figuring out the proof. That is, you have something you want to prove, but maybe it is easier to proving something more general or maybe your definitions need to change slightly. Anecdotally, during a project I spend perhaps a year figuring out exactly the right definition for a problem to be able to prove it. Of course, this was a very new thing. For well-know areas it is often straight forward, but at the frontier, both definitions and theorems often change as your proceed and understand the problem better.
Re: Why formalize mathematics – more than catching errors
#78Rado Kirov shows that formalization transforms how mathematicians think about structure and collaboration. My work begins from the same premise, but in the world of programming and system software. I aim to bring formal structure to programming itself, treating algorithms, operating systems, and programming languages as subjects that can be expressed with the same rigor as mathematics. I just released my treatise yes…
[deleted]
Re: Why formalize mathematics – more than catching errors
#79I’m not a mathematician, so could someone explain the difference in usage between Lean and Coq? On a surface level my understanding is that both are computer augmented ways to formalize mathematics. Why use one over the other? Why was Lean developed when Coq already existed?
I think the difference is mostly cultural. The type theories of Lean and Rocq are fairly close, with the exception that Lean operates with definitional proof irrelevance as one of the default axioms. This causes Lean to lose subject reduction and decidability of definitinal equality as properties of the language. Many people in the Rocq community see this as a no-go and some argue this will cause the system to be har…
> The type theories of Lean and Rocq are fairly close, with the exception that Lean operates with definitional proof irrelevance as one of the default axioms. This causes Lean to lose subject reduction and decidability of definitinal equality as properties of the language.
Couldn't you introduce proof relevance as an explicit axiom into a Lean program to solve that particular issue?
Re: Why formalize mathematics – more than catching errors
#80Earlier quoted context omitted.
LLMs and Lean are orthogonal, neither subsumes either. They both can be useful or harmful, do to their respective strengths and trade offs. PAC/statistical learning is good at needles in the haystack problems assuming that the tail losses, simplicity bias, and corpus representation issues are acceptable and you understand that it is fundamentally existential quantification and control for automation bias etc… Lean is…
> How Gödel’s second incompleteness theorem shows that you can prove anything, That is not at all what it says. > They both can be useful or harmful, If a proof is admitted into lean, there is no doubt as to its truth. There is no way in which lean can be construed as harmful. > The 2009 crash and gaussian copula as an example. There is nothing mathematical about the economics behind the 2009 crash. Such things are s…
> That is not at all what it says.
Gödel's incompleteness theorems demonstrate that any computable system that is sufficiently powerful, cannot be both consistent and syntactically complete.
Godel's second proved, a formula Con_κ associated with the consistency of κ is unprovable if κ is consistent.
If it is not consistent, Ex falso quodlibet (principle of explosion) applies and finding that contradiction allows any proposition or the negation of that proposition to be proven.
> They both can be useful or harmful
It is not lean that is harmful, mistaking finding a proof as being the same as truth. A proof that verifies a theorem does not have to explain why it holds, and the mathematical assumptions that may have been statistical is exactly why that failed.
Probability theory is just as much of a mathematical branch as λ-calculus. But we probably do differ in opinion on how "demonstrably true" much of mathematics is.
But here is a fairly accessible document related to the crash.
https://samueldwatts.com/wp-content/uploads/2016/08/Watts-Ga...