Hacker News Board Hacker News, browsed like a classic message board
Live data from Hacker News

Why formalize mathematics – more than catching errors

rkirov.github.io

Post reply on HN
Print view View original

51–60 of 80 posts

Re: Why formalize mathematics – more than catching errors

#51

Post by rpcope1 »

lo_zamoyski wrote: post #11
bwfan123 wrote: post #6

Earlier 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…

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.

Re: Why formalize mathematics – more than catching errors

#52

Post by lacker »

For anyone that's interested in formalizing mathematics but wished there was an easier way to do it, I've been working on a different sort of theorem prover recently.

https://acornprover.org

The idea is that there's a small AI built into the VS Code extension that will fill in the details of proofs for you. Check it out if you're interested in this sort of thing!

Re: Why formalize mathematics – more than catching errors

#53

Post by vonnik »

kronicum2025 wrote: post #21
vonnik wrote: post #10

Earlier quoted context omitted.

Out of curiosity, does anyone know the mathematicians actively leaning into AI + Lean?

I'm leaning a lot into AI + lean. It's a fantastic tool to find new proofs. The extremly rigid nature of lean means you can really check programs for correctness. So that part of AI is solved. The only thing that remains is generating proofs, and that is where there's nothing in AI space right now. As soon as we do get something, our mathematical knowledge is going to explode.

What kind of math do you do, and what would “generating proofs” look like do you think?

Re: Why formalize mathematics – more than catching errors

#54

Post by ljlolel »

constantcrying wrote: post #50
dboreham wrote: post #8

Earlier quoted context omitted.

Imho it was always "computerized", they just didn't have a computer. To me the approaches used in the early 20th century look like people defining a simple VM then writing programs that "execute" on that VM.

Exactly. The step to formalize mathematics through computation is just the logical consequence of the program of the formalizers. The idea actually goes back to Leibnitz, who was very much overoptimistic about computability, but already conceived of the idea of a logic machine, which could deter the truth value of any statement.

Which fell apart in shambles under Gödel

Re: Why formalize mathematics – more than catching errors

#56

Post by mprast »

dkural wrote: post #44

It's good to remind yourself of Bill Thurston's points: https://www.ams.org/journals/bull/1994-30-02/S0273-0979-1994... I love the analogy in David Bessis's wonderful book Mathematica (nothing to do with Wolfram). We all know how to tie our shoes. Now, write in words and symbols to teach someone how you tie your shoes. This is what a proof is. Often even people with STEM degrees confuse what mathematicians do with th…

I started having a much easier time with mathematics when I realized and got comfortable with this idea. In hindsight it should've been obvious to me as a programmer - when I'm building something, I don't ideate in terms of individual lines of code, after all

Re: Why formalize mathematics – more than catching errors

#57

Post by vesterthacker »

Rado 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 yesterday, at https://leanpub.com/elementsofprogramming

Elements of Programming presents programming as a mathematical discipline built on structure, logic, and proof. Written in the style of Euclid’s Elements, it defines computation through clear axioms, postulates, and propositions. Each book develops one aspect of programming as a coherent system of reasoning.

Book I establishes identity, transformation, and composition as the foundations of computation.

Book II introduces algebraic structures such as categories, functors, and monads.

Book III unites operational and denotational semantics to show that correctness means equivalence of meaning.

Book IV formalizes capability-based security and verification through invariants and confinement.

Book V connects type theory with formal assurance, explaining how types embody proofs.

Book VI extends these ideas into philosophy and ethics, arguing that software expresses human intention and responsibility.

Re: Why formalize mathematics – more than catching errors

#58

Post by jojomodding »

anonymousDan wrote: post #55

I don't get the point about trivial proofs. Can't you just tell Lean to assume something is true and then get on with the rest of the interesting part?

You can but that ruins the fun and also misses the point. How do you know your "trivial" theorem is actually trivial? Proofs are mechanized to increase our trust into them, and it defeats the point if you have to still manually review a myriad of helper lemmas.

Re: Why formalize mathematics – more than catching errors

#59

Post by jojomodding »

ljlolel wrote: post #54
constantcrying wrote: post #50

Earlier quoted context omitted.

Exactly. The step to formalize mathematics through computation is just the logical consequence of the program of the formalizers. The idea actually goes back to Leibnitz, who was very much overoptimistic about computability, but already conceived of the idea of a logic machine, which could deter the truth value of any statement.

Which fell apart in shambles under Gödel

Incredible, you managed to mention Gödel's incompleteness theorem on HN without wildly mis-stating what it's about ;)

Re: Why formalize mathematics – more than catching errors

#60

Post by confidantlake »

bwfan123 wrote: post #6
cbondurant wrote: post #4

Lean was a gamechanger for me as someone who has a "hobby" level interest in abstract mathematics. I don't have the formal education that would have cultivated the practice and repetition needed to just know on a gut level the kinds of formal manipulations needed for precise and accurate proofs. but lean (combined with its incredibly well designed abbreviation expansion) gives probably the most intuitive way to manip…

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.
Post reply on HN