9 ms·

Where is the fashionable mathematics?

85 points by karlicoss 7y ago

pg_is_a_butt 7y ago
YouTube videos about infinity and arbitrary base-10 oddities.
yters 7y ago
I feel like mathematicians should make the same effort for non mathematicians. Why do all these weird terms even matter to anyone else besides a self selected group of mathematicians? If they don't, why should anyone care about such things, just as the author asked why mathematicians should care about formal proof systems? Academia in general is so used to not having to justify their interests to anyone else that many seem to live in their own isolated little worlds. Gone are the days when the 'uni' in university meant a unified realm of knowledge. We should rename 'university' to be 'diversity.' However, the origin story of academia with Greek philosophy sought to not merely subsist in rapidly fracturing groups of special interest, but to also seek the unifying underlying ideas. Similarly with the scholastics in the medieval era, which actually birthed our university system. I believe academia has lost its way, which may spell its end. Which is unfortunate for our civilization, as it is so fundamentally tied to the quest for wisdom and knowledge.
- kragen 7y ago
  Why should mathematicians want non-mathematicians to care? The evidence to date shows that non-mathematicians do things like starting wars, electing Trump, dying of heroin overdoses, circulating conspiracy theories about climate change, sentencing Socrates to death, chopping down the Academy for firewood, putting Archimedes to the sword, burning the books and burying the scholars under Qin Shi Huang, burning Giordano Bruno, killing Galois in a duel, only recognizing Leonardo for his paintings, stripping the German Jewry of their professorships (those they didn't simply murder first, like Gödel's mentor Moritz Schlick), and drugging Turing until he grew breasts and killed himself. The best the mathematicians can hope for is to evade the attentions of the non-mathematicians so they can be left in peace with their theorems and their olive groves. The theorems are true and beautiful whether the non-mathematicians care or not. Governments burn libraries. Governments manifest the will of the common people. I, too, believe that academia has lost its way. Over the entry of the Academy it said, "Do not enter, non-geometers." We should return to that policy; allowing theologians and such peddlers of nonsense into the academy was an unavoidable concession during medieval times, but it is one we should walk back.
  - klyrs 7y ago
    Non-mathematicians build mathematics buildings, harvest and press chalk into sticks, grow the food and coffee we process into theorems (mathematicians are significantly more likely to od on amphetamines, btw), attend the calculus courses we desperately need for funding, clean our chalkboards and empty our wastebins... the list goes on and on. And yes there are mathematicians who vote for Trump. All you've proven with that tirade is a bound on the radius of your own filter bubble.
    - kragen 7y ago
      Mathematicians are perfectly capable of doing all those self-care things, as monks do in every monastery. (By contrast, non-mathematicians are unable to build anything larger than a small hut without help from mathematicians in the form of geometry.) I don't know of a single mathematician who has ODed on amphetamines, although of course amphetamines have been popular with mathematicians since they were discovered; and I know of only one who voted for Trump (Dan Kleitman), although undoubtedly others exist. The doses of amphetamines conducive to doing mathematics are about two orders of magnitude lower than the lethal doses, so it seems unlikely that someone who takes them to improve concentration rather than for euphoria would OD accidentally, as heroin users frequently do. Funding is only necessary to the extent that it helps keep the torch-wielding villagers away from the gate. To the extent that it subjects mathematical research to political tests, it is not only unnecessary, but counterproductive. If my filter bubble includes Bruno, Socrates, Mozi, Gödel, Turing, and Archimedes, I think its radius is adequate. I think the downvoting of my "tirade" to -2 has shown that non-mathematicians hate and fear mathematicians, think that all those killings of mathematicians I listed were reasonable and justified, and would like to silence any criticism of them.
      - JadeNB 7y ago
        > I don't know of a single mathematician who has ODed on amphetamines, and only one who voted for Trump (Dan Kleitman) I'm a mathematician who thinks that your sequence of posts here isn't serving the purpose you seem to think it does. I don't think that addressing it point by point serves much purpose, but these two claims bothered me particularly, so I single them out for response. I speak to your second point first: surely you don't think that there is only one mathematician who voted for Trump? Unless you do, it is irrelevant that you only know one; there are surely lots of others out there. I didn't, and I don't know any mathematician that I know did, but I know at least a few mathematicians who I know voted for GWB, and I imagine that there have to be at least a few other Trump voters in my mathematical circle. The first part in particular, in addition to the same quibble about what it matters whether or not you personally know such people (as opposed to whether or not they exist), probably requires an overly restrictive definition of 'mathematician' as "someone with academic credentials, or other official recognition, as a practitioner of mathematics". I personally don't think that's a good definition of a mathematician, and I don't think that advancing such definitions is a good thing for the future of our profession.
- bawolff 7y ago
  > Why do all these weird terms even matter to anyone else besides a self selected group of mathematicians? Why should anyone care about anything?
  - kragen 7y ago
    What is good, Wolff, and what is not good? How do we know these things?
- miscPerson 7y ago
  Mathematics is modern ontology. We’re not great at predicting which parts of ontology are eventually useful in other fields — mostly physics and other hard science, but more recently computer science, economics + finance, and even things like sociology and linguistics. So we let the people who self-select to be ontologists guide what the field researches — and this has generally been fairly effective. Certainly more effective than if we’d only looked at things which had immediate, obvious use. Complex numbers, widely used in science and engineering, were once regarded as suspect abstract nonsense. That’s why they’re called “imaginary numbers”: it was a pejorative name that stuck. We have cryptography, computers, modern physics, and modern finance to show for our efforts, among other things. It simply takes time (like, decades to centuries) for new ontological ideas to propagate to other fields. We’re hoping that formalizing into HoTT and other computer friendly systems will allow us to align with software development, and speed the process up. That seems to be going well, and at an accelerating pace. The hope is that HoTT and category theory give us a framework to do exactly what you propose — more easily specify and interlink knowledge. Expect results around 2050. It took around 40-60 years for category theory to have a big impact — but now it is in fields as far away from mathematics as linguistics. Hopefully HoTT will get there a little faster, but it’s still going to take decades to go from niche research to widely used in mathematics to widely used across disciplines. So, to summarize: 1. Because we’re bad at predicting the future and abstract math has often turned out to be useful later. 2. Mathematics is trying to do exactly what you propose with knowledge, via exactly the programs this blog is talking about.
  - yters 7y ago
    I disagree that all knowledge, or even the most important items of knoknowledge, are reducible to mathematics.
    - miscPerson 7y ago
      Could you explain why you disagree? I’d also accept an example of knowledge you don’t believe is expressible in mathematics.
  - kragen 7y ago
kragen 7y ago
Kevin Buzzard is doing really interesting work here, and I think that it's quite plausible that having fashionable mathematicians formalizing fashionable math in whatever proof assistant they choose will represent a significant step forward both for mathematical research and for the practice of programming, which is unavoidably formal in precisely the way math historically isn't. By formalizing it to that level, we will substantially increase our intellectual powers and make vast new fields tractable for formal reasoning, which also makes them tractable for programming. I'm not sure whether the beauty-contest winner will be LEAN (as Buzzard is promoting in this blog post), Metamath, or what. It may turn out that, say, Isabelle-HoTT or HoTT/Agda or something to pull ahead of LEAN, for example — certainly HoTT is a lot more fashionable among mathematicians than the CoC, and that might turn out to be either for a good reason (that manifests in technical advances in HoTT resulting in easier proofs) or a sufficiently strong social push to overcome the added friction. It's sure going to be interesting, though.
- prox 7y ago
  One of these questions I never dared to ask; What does formal mean in the area of mathematics? Is it like finalizing a formula / proof?
  - kragen 7y ago
    I'm not the ideal person to ask, never having published a novel mathematical result and not having particularly deep knowledge of math, but I understand "formal" in this context to mean "mechanical". A formal manipulation of symbols is, as I understand it, one that you can carry out without attaching any meaning to the symbols you are manipulating. This is not the same thing as "rigorous", because it's entirely possible for a formal manipulation to be unsound (with respect to some theory). For example, suppose you want to prove that a left multiplicative identity is also a right identity; that is, ∀x: 1·x = x ⇒ ∀x: x·1 = x. You can apply commutativity and rearrange the symbols to get a proof — that's a purely formal technique, and it's correct and rigorous for, say, complex-number multiplication. But if you're thinking of some other multiplication operations, like that of square matrices of some size, or of quaternions, that's not a rigorous proof, because those multiplication operations aren't commutative. (But in those cases it turns out to be a correct theorem anyway, because they are associative.) Compiling a program is another operation that is formal but rarely rigorous. The hope of using proof assistants in math is that by formalizing our reasoning, we can also make it more rigorous, with the aid of computers and a great deal of cleverness. Most mathematicians are not yet convinced.
nathias 7y ago
HoTT so hot right now...
- auggierose 7y ago
  But its inventor is really cold.
amvalo 7y ago
The answer is simple: these systems aren't mature enough to formalize the modern fashionable math. They need better ergonomics and perhaps better underlying theory before we attempt that.
- kragen 7y ago
  What would the better ergonomics look like? Do you have an idea what might be wrong with the theory?
  - amvalo 7y ago
    The biggest pain point with the theory was its handling of equality, which HoTT fixes. Ergonomically.. well it's hard to describe TBH, the easiest way to see is to just download one of these systems and try using them. You try to prove a theorem and everything just ends up taking way longer than you'd expect. Mostly because you can't gloss over small details the way mathematicians will do informally. Every small turn of phrase like "for large enough N" or "without loss of generality" can become dozens of extra lines of code.
    - kragen 7y ago
      I didn't mean to doubt your claim — my limited experience is that proof assistants are totally inscrutable, although I've been inspired by some of the Lean and Agda stuff I've been seeing lately. I just wanted to ask for your perspective, since it's probably more informed than mine! It seems to me that if you want to formalize the small details, you will necessarily have to do something different with some of those small details, won't you? Maybe a tactic search can find a formal and rigorous proof without you having to write those dozens of extra lines by hand, but simply glossing over them seems like it would defeat the goal of formalization.
- lonelappde 7y ago
  Another way to say that is that modern fashionable math is poorly founded and practitioners don't really know what are the fundamental things they are talking about.
zozbot234 7y ago
Not very surprising. When it comes to formal verification, you get the biggest bang for the buck (by far) via focusing on what the nLab wiki calls 'synthetic' mathematics, viz. fairly self-contained subfields where the 'rules of the game' may be somewhat complex in their own terms, but can be stated without relying on a massive amount of prereqs. 'Fashionable' math tends to be just the opposite: easy, logically-simple entailments, but building on very complex prereqs. It's obvious why formalizing the latter is comparatively hard: you need to work on the prerequisites first, since your formalization won't be usable without them! Also, since the formalized-math field is still quite fragmented, large projects (such as formalizing a big chunk of some basic curriculum) are discouraged to an even greater extent - quite simply, it can't be assumed that others will be building upon that work.
booleandilemma 7y ago
An article about fashionable mathematics and no mention of category theory?
- Koshkin 7y ago
  Here: https://ncatlab.org/nlab/show/Higher+Algebra https://ncatlab.org/nlab/show/Higher+Algebra Fascinating stuff explained in just over a thousand pages.
- madhadron 7y ago
  Category theory is an exciting, fashionable thing among some communities of programmers right now, but in mathematics it's just more tools at this point. Remember, MacLane's "Categories for the Working Mathematician" was published in 1971.
- neonate 7y ago
  In his famous talk from a few months ago he dismisses it as not-real-mathematics. I found it hard to tell whether he was being unironically provocative, trollish, or just cheeky.
  - kevinbuzzard 7y ago
    I was being intentionally provocative. On the other hand I feel like there are plenty of people in my (mathematics) department who would say that "normal" fields like geometry, topology, algebra, number theory and analysis are where the action is happening, and category theory is just a tool which we use to get "normal" maths done. On the other hand now Scholze is beginning to use infinity categories more in his work, this might change -- but it might not. Maybe in 10 years time there will be a book "infinity categories for the working mathematician" which we all read the first ten pages of and this is all that most of us need. Note that category theorists like Hyland and Johnstone have retired from Cambridge now and have not been replaced -- in the UK now you are more likely to find a category theorist working in a computer science department than a mathematics department. Whether or not it is "real mathematics", it is certainly a fact that in the UK at least it is an extremely small community, whereas our departments are full of number theorists, geometers, topologists, analysts and algebraists all of whom need to know essentially no category theory beyond the basic language of adjoint and representable functors.
dwheeler 7y ago
Article says: > 1. There is a large community of mathematicians out there who simply cannot join these communities because the learning curve is too high and much of the documentation is written for computer scientists. > 2. Even if a mathematician battles their way into one of these communities, there is a risk that they will not find the kind of mathematics which they are being taught, or teaching, in their own department, and there is a very big risk that they will not find much fashionable mathematics. > My explicit question to all the people in these formal proof verification communities is: what are you doing about this? I think many of the formal proof verification communities are trying to address these. I will focus on Metamath, especially its set.mm database that focuses on classical logic + ZFC ( http://us.metamath.org/mpeuni/mmset.html http://us.metamath.org/mpeuni/mmset.html ), but much of the following applies to all of them. I think the main problem is that too many mathematicians expect computer systems to have all the capabilities of a well-trained graduate mathematician. Yet the problem is hard. Computers are much better at some things (they don't get bored or sleepy), and humans are much better at other things (seeing the big picture & having insights into how to combine "unrelated" ideas). Much would be better if the formalization and traditional mathematics communities had more "meetings of the minds" & communication in general. Focusing on these questions: 1. The high learning curve is true for all systems, that's true. To be fair, mathematics has a high learning curve, you don't learn how to do it in a week. The problem is that although tools are very good at verifying formalized proofs, they are not great at coming up with the proofs themselves. I do agree that the documentation could be improved so "non computer scientists" could do things more easily. I think much of what's needed is for traditional mathematicians to engage with the formalization community, to make it clearer what's missing. There also needs to be work (and funding) on improved tooling, which implies a need for more funding (I'll discuss that below). 2. "They will not find much fashionable mathematics." There's a chicken-and-egg problem here. It takes a while to get proofs up to the "basics" of mathematics as expected by people work on "fashionable" mathematics. Here I think the solution is to have many people working to build up those basics. Take a look at my visualization of Metamath set.mm; note that it took many years for it to build up, and only when many people joined did it start seriously growing: https://www.youtube.com/watch?v=XC1g8FmFcUU https://www.youtube.com/watch?v=XC1g8FmFcUU The real bottom line is that there really needs to be more funding on tools & formalized systems. Metamath isn't funded at all to my knowledge. Lean and Coq have some funding, but nothing like the funding of many other fields. We should be impressed about how far they've come in spite of that. A broader problem is that mathematicians typically accept a proof if a paper seems to be okay to another mathematician. When the math and proofs were simpler, that was probably fine, and since computers weren't very capable that's all we could do anyway. But today's math (and proofs) are far more complex, and it's becoming absurd to leave that as our standard of proof. Computers are available now; we should be using them.
Koshkin 7y ago
Looks like Geometric Algebra is something that has been talked about quite a lot lately. (It is "vector algebra done right.")
- madhadron 7y ago
  Geometric algebra is something that hasn't found a "killer app," if you will. The largest users of vector calculus are physicists and engineers, and those communities have 1) enormous existing literature using Gibbs-Heaviside vectors, and 2) enormous institutional investment in teaching them across departments. We haven't found a justification for switching that would outweigh the amount of inertia involved. It's hardly a new thing. David Hestenes has been writing books about its advantages in physics since the 1960's.
- lonelappde 7y ago
  That's fashionable computer science, not fashionable mathematics. In math it's a minor alternative formulation for a relatively concrete (aka boring) topic. (coordinate vectors).
dang 7y ago
Related from last year: https://news.ycombinator.com/item?id=21200721 https://news.ycombinator.com/item?id=21200721 https://news.ycombinator.com/item?id=20909404 https://news.ycombinator.com/item?id=20909404
kalyantm 7y ago
A little off topic, I'm genuinely interested in diving into Math again. Never appreciated it in college (Comp Sci Engineering, had the first year with some engineering maths) but now i really want to get into it again. (Calculas, trignometry and statistics) Can anyone point me to resources/path on how/where to begin?
- kragen 7y ago
  I've been finding it useful to audit university classes. Do you have a university nearby?
- drchewbacca 7y ago
  If you can program you might like Metamath, it feels quite a lot like writing code. Here is the main site. http://us.metamath.org/index.html http://us.metamath.org/index.html Here is the book which can help with understanding. http://us.metamath.org/downloads/metamath.pdf http://us.metamath.org/downloads/metamath.pdf Here are some tutorials for MMJ2 which is the main proof assistant to use, https://www.youtube.com/playlist?list=PL1jSu6GGefBm7RBP0Id2Sa9uyVuyhioAC https://www.youtube.com/playlist?list=PL1jSu6GGefBm7RBP0Id2S... it can be found here, http://us.metamath.org/#mmj2 http://us.metamath.org/#mmj2 Here are some beginners proof exercises which are a good place to start out http://us.metamath.org/mpegif/mmtheorems289.html#mm28844b http://us.metamath.org/mpegif/mmtheorems289.html#mm28844b I will warn you though it is a bit like the wild west, it is not easy to accomplish anything and it is exciting to be on the frontier. The community is really cool, you can chat with them here. https://groups.google.com/forum/#!forum/metamath https://groups.google.com/forum/#!forum/metamath
kenkubota 7y ago
My comment on Kevin Buzzard's intervention: https://groups.google.com/d/msg/metamath/Fgn0qZEzCko/bvVem1BZCQAJ https://groups.google.com/d/msg/metamath/Fgn0qZEzCko/bvVem1B... Link list of the discussion threads: https://owlofminerva.net/kubota/update-to-the-foundations-of-mathematics/ https://owlofminerva.net/kubota/update-to-the-foundations-of...

85 points by karlicoss 7y ago

YouTube videos about infinity and arbitrary base-10 oddities.

I feel like mathematicians should make the same effort for non mathematicians. Why do all these weird terms even matter to anyone else besides a self selected group of mathematicians? If they don't, why should anyone care about such things, just as the author asked why mathematicians should care about formal proof systems? Academia in general is so used to not having to justify their interests to anyone else that many seem to live in their own isolated little worlds. Gone are the days when the 'uni' in university meant a unified realm of knowledge. We should rename 'university' to be 'diversity.' However, the origin story of academia with Greek philosophy sought to not merely subsist in rapidly fracturing groups of special interest, but to also seek the unifying underlying ideas. Similarly with the scholastics in the medieval era, which actually birthed our university system. I believe academia has lost its way, which may spell its end. Which is unfortunate for our civilization, as it is so fundamentally tied to the quest for wisdom and knowledge.

kragen 7y ago
Why should mathematicians want non-mathematicians to care? The evidence to date shows that non-mathematicians do things like starting wars, electing Trump, dying of heroin overdoses, circulating conspiracy theories about climate change, sentencing Socrates to death, chopping down the Academy for firewood, putting Archimedes to the sword, burning the books and burying the scholars under Qin Shi Huang, burning Giordano Bruno, killing Galois in a duel, only recognizing Leonardo for his paintings, stripping the German Jewry of their professorships (those they didn't simply murder first, like Gödel's mentor Moritz Schlick), and drugging Turing until he grew breasts and killed himself. The best the mathematicians can hope for is to evade the attentions of the non-mathematicians so they can be left in peace with their theorems and their olive groves. The theorems are true and beautiful whether the non-mathematicians care or not. Governments burn libraries. Governments manifest the will of the common people. I, too, believe that academia has lost its way. Over the entry of the Academy it said, "Do not enter, non-geometers." We should return to that policy; allowing theologians and such peddlers of nonsense into the academy was an unavoidable concession during medieval times, but it is one we should walk back.
- klyrs 7y ago
  Non-mathematicians build mathematics buildings, harvest and press chalk into sticks, grow the food and coffee we process into theorems (mathematicians are significantly more likely to od on amphetamines, btw), attend the calculus courses we desperately need for funding, clean our chalkboards and empty our wastebins... the list goes on and on. And yes there are mathematicians who vote for Trump. All you've proven with that tirade is a bound on the radius of your own filter bubble.
  - kragen 7y ago
    Mathematicians are perfectly capable of doing all those self-care things, as monks do in every monastery. (By contrast, non-mathematicians are unable to build anything larger than a small hut without help from mathematicians in the form of geometry.) I don't know of a single mathematician who has ODed on amphetamines, although of course amphetamines have been popular with mathematicians since they were discovered; and I know of only one who voted for Trump (Dan Kleitman), although undoubtedly others exist. The doses of amphetamines conducive to doing mathematics are about two orders of magnitude lower than the lethal doses, so it seems unlikely that someone who takes them to improve concentration rather than for euphoria would OD accidentally, as heroin users frequently do. Funding is only necessary to the extent that it helps keep the torch-wielding villagers away from the gate. To the extent that it subjects mathematical research to political tests, it is not only unnecessary, but counterproductive. If my filter bubble includes Bruno, Socrates, Mozi, Gödel, Turing, and Archimedes, I think its radius is adequate. I think the downvoting of my "tirade" to -2 has shown that non-mathematicians hate and fear mathematicians, think that all those killings of mathematicians I listed were reasonable and justified, and would like to silence any criticism of them.
    - JadeNB 7y ago
      > I don't know of a single mathematician who has ODed on amphetamines, and only one who voted for Trump (Dan Kleitman) I'm a mathematician who thinks that your sequence of posts here isn't serving the purpose you seem to think it does. I don't think that addressing it point by point serves much purpose, but these two claims bothered me particularly, so I single them out for response. I speak to your second point first: surely you don't think that there is only one mathematician who voted for Trump? Unless you do, it is irrelevant that you only know one; there are surely lots of others out there. I didn't, and I don't know any mathematician that I know did, but I know at least a few mathematicians who I know voted for GWB, and I imagine that there have to be at least a few other Trump voters in my mathematical circle. The first part in particular, in addition to the same quibble about what it matters whether or not you personally know such people (as opposed to whether or not they exist), probably requires an overly restrictive definition of 'mathematician' as "someone with academic credentials, or other official recognition, as a practitioner of mathematics". I personally don't think that's a good definition of a mathematician, and I don't think that advancing such definitions is a good thing for the future of our profession.
bawolff 7y ago
> Why do all these weird terms even matter to anyone else besides a self selected group of mathematicians? Why should anyone care about anything?
- kragen 7y ago
  What is good, Wolff, and what is not good? How do we know these things?
miscPerson 7y ago
Mathematics is modern ontology. We’re not great at predicting which parts of ontology are eventually useful in other fields — mostly physics and other hard science, but more recently computer science, economics + finance, and even things like sociology and linguistics. So we let the people who self-select to be ontologists guide what the field researches — and this has generally been fairly effective. Certainly more effective than if we’d only looked at things which had immediate, obvious use. Complex numbers, widely used in science and engineering, were once regarded as suspect abstract nonsense. That’s why they’re called “imaginary numbers”: it was a pejorative name that stuck. We have cryptography, computers, modern physics, and modern finance to show for our efforts, among other things. It simply takes time (like, decades to centuries) for new ontological ideas to propagate to other fields. We’re hoping that formalizing into HoTT and other computer friendly systems will allow us to align with software development, and speed the process up. That seems to be going well, and at an accelerating pace. The hope is that HoTT and category theory give us a framework to do exactly what you propose — more easily specify and interlink knowledge. Expect results around 2050. It took around 40-60 years for category theory to have a big impact — but now it is in fields as far away from mathematics as linguistics. Hopefully HoTT will get there a little faster, but it’s still going to take decades to go from niche research to widely used in mathematics to widely used across disciplines. So, to summarize: 1. Because we’re bad at predicting the future and abstract math has often turned out to be useful later. 2. Mathematics is trying to do exactly what you propose with knowledge, via exactly the programs this blog is talking about.
- yters 7y ago
  I disagree that all knowledge, or even the most important items of knoknowledge, are reducible to mathematics.
  - miscPerson 7y ago
    Could you explain why you disagree? I’d also accept an example of knowledge you don’t believe is expressible in mathematics.
- kragen 7y ago

kragen 7y ago

Kevin Buzzard is doing really interesting work here, and I think that it's quite plausible that having fashionable mathematicians formalizing fashionable math in whatever proof assistant they choose will represent a significant step forward both for mathematical research and for the practice of programming, which is unavoidably formal in precisely the way math historically isn't. By formalizing it to that level, we will substantially increase our intellectual powers and make vast new fields tractable for formal reasoning, which also makes them tractable for programming. I'm not sure whether the beauty-contest winner will be LEAN (as Buzzard is promoting in this blog post), Metamath, or what. It may turn out that, say, Isabelle-HoTT or HoTT/Agda or something to pull ahead of LEAN, for example — certainly HoTT is a lot more fashionable among mathematicians than the CoC, and that might turn out to be either for a good reason (that manifests in technical advances in HoTT resulting in easier proofs) or a sufficiently strong social push to overcome the added friction. It's sure going to be interesting, though.

prox 7y ago
One of these questions I never dared to ask; What does formal mean in the area of mathematics? Is it like finalizing a formula / proof?
- kragen 7y ago
  I'm not the ideal person to ask, never having published a novel mathematical result and not having particularly deep knowledge of math, but I understand "formal" in this context to mean "mechanical". A formal manipulation of symbols is, as I understand it, one that you can carry out without attaching any meaning to the symbols you are manipulating. This is not the same thing as "rigorous", because it's entirely possible for a formal manipulation to be unsound (with respect to some theory). For example, suppose you want to prove that a left multiplicative identity is also a right identity; that is, ∀x: 1·x = x ⇒ ∀x: x·1 = x. You can apply commutativity and rearrange the symbols to get a proof — that's a purely formal technique, and it's correct and rigorous for, say, complex-number multiplication. But if you're thinking of some other multiplication operations, like that of square matrices of some size, or of quaternions, that's not a rigorous proof, because those multiplication operations aren't commutative. (But in those cases it turns out to be a correct theorem anyway, because they are associative.) Compiling a program is another operation that is formal but rarely rigorous. The hope of using proof assistants in math is that by formalizing our reasoning, we can also make it more rigorous, with the aid of computers and a great deal of cleverness. Most mathematicians are not yet convinced.

nathias 7y ago

HoTT so hot right now...

auggierose 7y ago
But its inventor is really cold.

amvalo 7y ago

The answer is simple: these systems aren't mature enough to formalize the modern fashionable math. They need better ergonomics and perhaps better underlying theory before we attempt that.

kragen 7y ago
What would the better ergonomics look like? Do you have an idea what might be wrong with the theory?
- amvalo 7y ago
  The biggest pain point with the theory was its handling of equality, which HoTT fixes. Ergonomically.. well it's hard to describe TBH, the easiest way to see is to just download one of these systems and try using them. You try to prove a theorem and everything just ends up taking way longer than you'd expect. Mostly because you can't gloss over small details the way mathematicians will do informally. Every small turn of phrase like "for large enough N" or "without loss of generality" can become dozens of extra lines of code.
  - kragen 7y ago
    I didn't mean to doubt your claim — my limited experience is that proof assistants are totally inscrutable, although I've been inspired by some of the Lean and Agda stuff I've been seeing lately. I just wanted to ask for your perspective, since it's probably more informed than mine! It seems to me that if you want to formalize the small details, you will necessarily have to do something different with some of those small details, won't you? Maybe a tactic search can find a formal and rigorous proof without you having to write those dozens of extra lines by hand, but simply glossing over them seems like it would defeat the goal of formalization.
lonelappde 7y ago
Another way to say that is that modern fashionable math is poorly founded and practitioners don't really know what are the fundamental things they are talking about.

zozbot234 7y ago

Not very surprising. When it comes to formal verification, you get the biggest bang for the buck (by far) via focusing on what the nLab wiki calls 'synthetic' mathematics, viz. fairly self-contained subfields where the 'rules of the game' may be somewhat complex in their own terms, but can be stated without relying on a massive amount of prereqs. 'Fashionable' math tends to be just the opposite: easy, logically-simple entailments, but building on very complex prereqs. It's obvious why formalizing the latter is comparatively hard: you need to work on the prerequisites first, since your formalization won't be usable without them! Also, since the formalized-math field is still quite fragmented, large projects (such as formalizing a big chunk of some basic curriculum) are discouraged to an even greater extent - quite simply, it can't be assumed that others will be building upon that work.

booleandilemma 7y ago

An article about fashionable mathematics and no mention of category theory?

Koshkin 7y ago
Here: https://ncatlab.org/nlab/show/Higher+Algebra https://ncatlab.org/nlab/show/Higher+Algebra Fascinating stuff explained in just over a thousand pages.
madhadron 7y ago
Category theory is an exciting, fashionable thing among some communities of programmers right now, but in mathematics it's just more tools at this point. Remember, MacLane's "Categories for the Working Mathematician" was published in 1971.
neonate 7y ago
In his famous talk from a few months ago he dismisses it as not-real-mathematics. I found it hard to tell whether he was being unironically provocative, trollish, or just cheeky.
- kevinbuzzard 7y ago
  I was being intentionally provocative. On the other hand I feel like there are plenty of people in my (mathematics) department who would say that "normal" fields like geometry, topology, algebra, number theory and analysis are where the action is happening, and category theory is just a tool which we use to get "normal" maths done. On the other hand now Scholze is beginning to use infinity categories more in his work, this might change -- but it might not. Maybe in 10 years time there will be a book "infinity categories for the working mathematician" which we all read the first ten pages of and this is all that most of us need. Note that category theorists like Hyland and Johnstone have retired from Cambridge now and have not been replaced -- in the UK now you are more likely to find a category theorist working in a computer science department than a mathematics department. Whether or not it is "real mathematics", it is certainly a fact that in the UK at least it is an extremely small community, whereas our departments are full of number theorists, geometers, topologists, analysts and algebraists all of whom need to know essentially no category theory beyond the basic language of adjoint and representable functors.

dwheeler 7y ago

Article says: > 1. There is a large community of mathematicians out there who simply cannot join these communities because the learning curve is too high and much of the documentation is written for computer scientists. > 2. Even if a mathematician battles their way into one of these communities, there is a risk that they will not find the kind of mathematics which they are being taught, or teaching, in their own department, and there is a very big risk that they will not find much fashionable mathematics. > My explicit question to all the people in these formal proof verification communities is: what are you doing about this? I think many of the formal proof verification communities are trying to address these. I will focus on Metamath, especially its set.mm database that focuses on classical logic + ZFC ( http://us.metamath.org/mpeuni/mmset.html http://us.metamath.org/mpeuni/mmset.html ), but much of the following applies to all of them. I think the main problem is that too many mathematicians expect computer systems to have all the capabilities of a well-trained graduate mathematician. Yet the problem is hard. Computers are much better at some things (they don't get bored or sleepy), and humans are much better at other things (seeing the big picture & having insights into how to combine "unrelated" ideas). Much would be better if the formalization and traditional mathematics communities had more "meetings of the minds" & communication in general. Focusing on these questions: 1. The high learning curve is true for all systems, that's true. To be fair, mathematics has a high learning curve, you don't learn how to do it in a week. The problem is that although tools are very good at verifying formalized proofs, they are not great at coming up with the proofs themselves. I do agree that the documentation could be improved so "non computer scientists" could do things more easily. I think much of what's needed is for traditional mathematicians to engage with the formalization community, to make it clearer what's missing. There also needs to be work (and funding) on improved tooling, which implies a need for more funding (I'll discuss that below). 2. "They will not find much fashionable mathematics." There's a chicken-and-egg problem here. It takes a while to get proofs up to the "basics" of mathematics as expected by people work on "fashionable" mathematics. Here I think the solution is to have many people working to build up those basics. Take a look at my visualization of Metamath set.mm; note that it took many years for it to build up, and only when many people joined did it start seriously growing: https://www.youtube.com/watch?v=XC1g8FmFcUU https://www.youtube.com/watch?v=XC1g8FmFcUU The real bottom line is that there really needs to be more funding on tools & formalized systems. Metamath isn't funded at all to my knowledge. Lean and Coq have some funding, but nothing like the funding of many other fields. We should be impressed about how far they've come in spite of that. A broader problem is that mathematicians typically accept a proof if a paper seems to be okay to another mathematician. When the math and proofs were simpler, that was probably fine, and since computers weren't very capable that's all we could do anyway. But today's math (and proofs) are far more complex, and it's becoming absurd to leave that as our standard of proof. Computers are available now; we should be using them.

Koshkin 7y ago

Looks like Geometric Algebra is something that has been talked about quite a lot lately. (It is "vector algebra done right.")

madhadron 7y ago
Geometric algebra is something that hasn't found a "killer app," if you will. The largest users of vector calculus are physicists and engineers, and those communities have 1) enormous existing literature using Gibbs-Heaviside vectors, and 2) enormous institutional investment in teaching them across departments. We haven't found a justification for switching that would outweigh the amount of inertia involved. It's hardly a new thing. David Hestenes has been writing books about its advantages in physics since the 1960's.
lonelappde 7y ago
That's fashionable computer science, not fashionable mathematics. In math it's a minor alternative formulation for a relatively concrete (aka boring) topic. (coordinate vectors).

dang 7y ago

Related from last year: https://news.ycombinator.com/item?id=21200721 https://news.ycombinator.com/item?id=21200721 https://news.ycombinator.com/item?id=20909404 https://news.ycombinator.com/item?id=20909404

kalyantm 7y ago

A little off topic, I'm genuinely interested in diving into Math again. Never appreciated it in college (Comp Sci Engineering, had the first year with some engineering maths) but now i really want to get into it again. (Calculas, trignometry and statistics) Can anyone point me to resources/path on how/where to begin?

kragen 7y ago
I've been finding it useful to audit university classes. Do you have a university nearby?
drchewbacca 7y ago
If you can program you might like Metamath, it feels quite a lot like writing code. Here is the main site. http://us.metamath.org/index.html http://us.metamath.org/index.html Here is the book which can help with understanding. http://us.metamath.org/downloads/metamath.pdf http://us.metamath.org/downloads/metamath.pdf Here are some tutorials for MMJ2 which is the main proof assistant to use, https://www.youtube.com/playlist?list=PL1jSu6GGefBm7RBP0Id2Sa9uyVuyhioAC https://www.youtube.com/playlist?list=PL1jSu6GGefBm7RBP0Id2S... it can be found here, http://us.metamath.org/#mmj2 http://us.metamath.org/#mmj2 Here are some beginners proof exercises which are a good place to start out http://us.metamath.org/mpegif/mmtheorems289.html#mm28844b http://us.metamath.org/mpegif/mmtheorems289.html#mm28844b I will warn you though it is a bit like the wild west, it is not easy to accomplish anything and it is exciting to be on the frontier. The community is really cool, you can chat with them here. https://groups.google.com/forum/#!forum/metamath https://groups.google.com/forum/#!forum/metamath

kenkubota 7y ago

My comment on Kevin Buzzard's intervention: https://groups.google.com/d/msg/metamath/Fgn0qZEzCko/bvVem1BZCQAJ https://groups.google.com/d/msg/metamath/Fgn0qZEzCko/bvVem1B... Link list of the discussion threads: https://owlofminerva.net/kubota/update-to-the-foundations-of-mathematics/ https://owlofminerva.net/kubota/update-to-the-foundations-of...