Kevin Buzzard
2024 · arXiv
We discuss how the concept of equality is used by mathematicians (including Grothendieck), and what effect this has when trying to formalise mathematics. We challenge various reasonable-sounding slogans about equality.
Metadata: arXiv. Abstracts retain their original authors’ rights.
Original HN comments, with labels from simple text rules. A label describes the whole comment and may miss context or irony. Read the discussion to make up your own mind. About the labels
4 selected excerpts · 4 total mentions
Interestingly, the way in which Grothendieck conceived of equality is nowadays being questioned, especially due to the rise of formalized mathematics and Lean. More concretely, there is this fun paper by Kevin Buzzard which deconstructs it: https://arxiv.org/abs/2405.10387 Money quote: > In this paper I argue that the first assertion above is false, the second is dan- gerous, and the third is meaningless.
> HoTT is a highly technical, highly niche topic and it doesn't make sense to tackle two ambitious projects at the same time like this. It's also a bit of a controversial topic in formalized mathematics. See the following relevant comments by Kevin Buzzard (an expert in Lean and also in the sort of abstract nonsense that might arguably benefit directly from HoTT) - Links courtesy of https://ncatlab.org/nlab/show/Kevin+Buzzard * Is HoTT the way to do mathematics? (2020) https://www.cl.cam.ac.uk/events/owls/slides/buzzard.pdf ("Nobody knows because nobody tried") * Grothendieck's use of equality (2024) https://arxiv.org/abs/2405.10387 - Discussed here https://news.ycombinator.com/item?id=40414404
Pi is transcendental but computable. For an introduction to real real analysis is an old book typically called the 'Baby Rudin' Principles of Mathematical Analysis by Walter Rudin. It is tiny and expensive, as most college math text books are once you get past a certain level. No idea if there is something better now, it is from the 1950's and there are used copies in most used book shops for cheap (or there was). It has no definition of 'equals' but does have a concept of equivalent relations. Dummit and Foote's Abstract Algebra book is a great reference, especially with the problem with AI pollution. Coming from a General Relativity background, it still took me two…
years to work through on my own. I don't know any suggestions on a more modern approach of starting with type or category theory. I am not really interested in constructivist math, it is a problem to get around for me, so maybe someone who is can chime in on a better path. While not rigorous, this paper does a good job at explaining just how muddy the concept of 'equality' is. https://arxiv.org/abs/2405.10387
I do not have time now but I intend to read this soon. Link to paper: https://arxiv.org/pdf/2405.10387 It is a nice looking article that about how we use the eual sign in mathematics and computer science. I do not look a popularmechanics much (not really since the early 80s). his one looks good. I would like to know hat others think.
More from the same topics.
William P. Thurston
In response to Jaffe and Quinn [math.HO/9307227], the author discusses forms of progress in mathematics that are not captured by formal proofs of theorems, especially in his own work in the theory of foliations and geometrization of 3-manifolds and dynamical systems.
Sébastien Bubeck, Varun Chandrasekaran, Ronen Eldan +11
Artificial intelligence (AI) researchers have been developing and refining large language models (LLMs) that exhibit remarkable capabilities across a variety of domains and tasks, challenging our understanding of learning and cognition.
Martin Kleppmann
The CAP Theorem is a frequently cited impossibility result in distributed systems, especially among NoSQL distributed databases.
Eric Chisolm
This is an introduction to geometric algebra, an alternative to traditional vector algebra that expands on it in two ways: 1.