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

11–20 of 80 posts

Re: Why formalize mathematics – more than catching errors

#11

Post by lo_zamoyski »

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…

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 of natural language itself.)

No formalism is ontologically neutral in the sense that there is always an implied ontology or range of possible ontologies. 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.

Re: Why formalize mathematics – more than catching errors

#12

Post by thechao »

vonnik wrote: post #10
oersted wrote: post #3

I've been excited about Lean for years, not because of correctness guarantees, but because it opens the door to doing maths using software development methods. Libraries of theorems and mathematical objects, with well defined abstractions that are ergonomic to apply in target use cases. Accompanied by good documentation, focused less on how the theorems are proven (how the functions are implemented), and more on what…

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

Terence Tao posts on mathstodon fairly regularly about lean, AI, and math. I'm not going to interpret his posts.

Re: Why formalize mathematics – more than catching errors

#13

Post by oersted »

vonnik wrote: post #10
oersted wrote: post #3

I've been excited about Lean for years, not because of correctness guarantees, but because it opens the door to doing maths using software development methods. Libraries of theorems and mathematical objects, with well defined abstractions that are ergonomic to apply in target use cases. Accompanied by good documentation, focused less on how the theorems are proven (how the functions are implemented), and more on what…

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

Terence Tao is well known for being enthusiastic about Lean and AI and he regularly posts about his experiments.

He is also a serious research mathematician at the top of his game, considered by many one of the best mathematicians alive. This might be biased by the fact that he is such a good communicator, he is more visible than other similarly good mathematicians, but he is a Fields medallist all the same.

Re: Why formalize mathematics – more than catching errors

#14

Post by KalMann »

I want to respond to each of his points one by one

> powering various math tools

I don't think going through a math proof like they were computer programs is a good way to approach mathematics. In mathematics I think the important thing is developing a good intuition and mental model of the material. It's not a huge problem if the proof isn't 100% complete or correct if the general approach is good. Unlike programming, where you need a program to work 99.9% of the time, you have to pay close attention to all the minute details.

> analyzing meta-math trends

I'm highly skeptical of the usefulness of this approach in identifying non-trivial trends. In mathematics the same kinds of principles can appear in many different forms, and you won't necessarily use the same language or cite the same theorems even though the parallels are clear to those who understand them. Perhaps LLMs with their impressive reasoning abilities can identify parallels but I doubt a simple program would yield useful insights.

> Basically, the process of doing math will become more efficient and hopefully more pleasant.

I don't see how his points make things more efficient. It seems like it's adding a bunch more work. It definitely doesn't sound more pleasant.

Re: Why formalize mathematics – more than catching errors

#15

Post by westurner »

> While Paulson focuses on the obvious benefit of finding potential errors in proofs as they are checked by a computer, I will discuss some other less obvious benefits of shifting to formal math or “doing math with computers”

From https://news.ycombinator.com/item?id=44214804 sort of re: Tao's Real Analysis formalisms:

> So, Lean isn't proven with HoTT either.

Re: Why formalize mathematics – more than catching errors

#16

Post by pfdietz »

Another reason to formalize math is that formalized proofs become training material for automated mathematics.

Ultimately we want all of the math literature to become training material, but that would likely require automated techniques for converting it to formalized proofs. This would be a back-and-forth thing that would build on itself.

Re: Why formalize mathematics – more than catching errors

#17

Post by nyrikki »

anon291 wrote: post #9
oersted wrote: post #3

I've been excited about Lean for years, not because of correctness guarantees, but because it opens the door to doing maths using software development methods. Libraries of theorems and mathematical objects, with well defined abstractions that are ergonomic to apply in target use cases. Accompanied by good documentation, focused less on how the theorems are proven (how the functions are implemented), and more on what…

As a a hobbyist mathematician / type theorist, chatgpt et al are great at 'looking up' theorems that you want to exist but that you may not have read about yet. It's also good at connecting disparate areas of math. I don't think lean subsumes AI. Rather, lean allows you to check the AI proof. ChatGPT genuinely does have a knack for certain lines of thought.

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 a wonderful collection of concepts and heuristics but due to Rice and Gödel etc… will not solve all problems with software development.

How Gödel’s second incompleteness theorem shows that you can prove anything, without that proof being meaningful is a lens into that.

It is horses for courses, and remember that even in sub-TC total functional programming, proving and arbitrary functions is very hard, while constructing one is far more tractable.

Even those proofs don’t demonstrate semantic correctness. History is riddled with examples of people using powerful tools that elegantly explain flawed beliefs.

The 2009 crash and gaussian copula as an example.

Get all the value you can out of these tools, but use caution, especially in math, where superficially similar similarities often have conflicting conventions, constraints, and assumptions.

Obviously if you problem is ergotic with the Markov property, both will help, but Automated theorem proving and PAC learning will never be a meta theory of the other IMHO.

Re: Why formalize mathematics – more than catching errors

#19

Post by umutisik »

As a former professional mathematician: the benefits mentioned in the article (click-through definitions and statements, analyzing meta trends, version control, ...) do not seem particularly valuable.

The reason to formalize mathematics is to automate mathematical proofs and the production of mathematical theory.

Re: Why formalize mathematics – more than catching errors

#20

Post by griffzhowl »

vonnik wrote: post #10
oersted wrote: post #3

I've been excited about Lean for years, not because of correctness guarantees, but because it opens the door to doing maths using software development methods. Libraries of theorems and mathematical objects, with well defined abstractions that are ergonomic to apply in target use cases. Accompanied by good documentation, focused less on how the theorems are proven (how the functions are implemented), and more on what…

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

Kevin Buzzard has been the main mathematician involved with Lean

This is a recent talk where he discusses putting it together with LLMs (he's somewhat sceptical it'll be revolutionary for producing new mathematics any time soon)

https://www.youtube.com/watch?v=K5w7VS2sxD0

Post reply on HN