arXiv:2405.10387math.AG
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.
Linked by 4 identifiable commenters in 4 comments across 4 threads, from Jul 2024 to May 2026. Found in 1 HN submission from May 2024 to May 2024. Open submission discussions.
> 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…
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.…
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).…
Connected through shared HN threads, not inferred similarity or a recommendation.
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…
jojomoddingView on HNParent context