> 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 ), 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
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.
If I understand the context correctly, Buzzard wrote this post as a step toward solving the problems you state (mathematicians are unconvinced of the usefulness of proof assistants, many people need to join in to build things up in a proof assistant, documentation needs work, input from mathematicians is needed).
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.
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.
Rigor means not hand-waving about things that a skeptic might doubt, not skipping corner cases, etc.
Formal means doing things like a computer -- strictly symbolic analysis that doesn't claim to do the impossible task accurately map back to our informal ideas of what things mean.
Formality is across a chasm -- it's the most accurate kind of math we can do, but it can't be trusted to say that a formal proof about say complex numbers actually applies to what you are thinking about when you day "complex numbers".
As is said, "It is impossible to pass from the informal by purely formal means."
This is in accordance with my understanding, but since you seem to think I was saying something different, I think your expression of it is clearer than mine was.
Thanks for sharing your thoughts, so if I get it right, you give me a formula that has been formalized, and I just punch in the right numbers for the variables and get the answer.
The less rigorously the arrangement (and proofed) , the more likely the outcome is wrong though the syntax (symbol manipulation) is correct.
If you're using a proof assistant, you can't just write something like "X clearly follows from Y" or "Z is left as an exercise to the reader": you have to specify every step, even if they're steps a human reader would easily figure out themselves.
What logicchains says above is true in some sense but of course it depends on the degree of automation a given theorem proving environment provides. In Isabelle a proof may consist of the keyword "using" followed by a list o 9-10 theorems and it may be accepted if the list is complete (in some sense).
That's definitely true, but unfortunately I think the set of things "left to the reader" is way larger than the set of things Isabelle can figure out by itself, even with Sledgehammer.
Of course you can! You can put any axioms (a claim that a conjecture is true is an axiom) you want in a proof assistant. What you cannot do is not say those things but still rely on them in your proof.
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.
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.
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.
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.
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.
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?
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.
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.
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.
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.
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).
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.
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.
While this is factually true, as a normative statement it represents an inversion of priorities, like attending school so that you can have a summer vacation, admiring Michelangelo's art because of how much reputation the Medicis gained by patronizing it, or hoping your mother will get a better job so that she can buy you more candy. It trivializes mathematics.
It's true that we only have cryptography, computers, physics, and finance — and not only the modern kind — because of the human study of mathematics. But cryptography and finance are of distinctly tertiary importance, computers and physics of secondary importance, and mathematics of primary importance. So it is nonsense to say that mathematics is important because it helps us understand physics. Mathematics is important because it transcends physics; the same mathematical theories would be consistent in a universe with totally different physics. Their beauty does not depend on whether or not they happen to describe the physics in a particular universe or not.
The Pythagorean Theorem was discovered by the humans in Mesopotamia somewhere between 3500 and 5000 years ago; nobody knows who discovered it. (Pythagoras wouldn't be born for centuries.) It was used to design buildings, but the buildings have been worn to dust. It was used then to divide up farmland, but the farmers are dead, their bones have worn away to dust in the sand, their names are mostly forgotten, and their farmland turned to desert. But the knowledge of the theorem, and the place-value number system the Babylonians invented, has endured, and the humans still divide the circle into 360 degrees, each degree into 60 minutes, and each minute into 60 seconds, a tradition inherited from the Babylonians.
Moreover, the stars and planets have moved in a way described by the Pythagorean Theorem since there have been planets and stars, for almost 14 billion of the time unit that would eventually be a "year" on Earth. And, most likely, they will continue to do so for as long as there are planets and stars; and as long as there are humans, they will know the Pythagorean Theorem, even if the name of Babylon is forgotten.
Today the humans consider cryptography important because it governs the rise and fall of nations and empires; they consider finance important because it governs the rise and fall of firms, and decides which humans are powerful and which humans are poor and starving. But, it is nearly certain that all of those powerful humans will be dead in a century and a half, and all of those nations and empires will be gone in a millennium.
But, if libraries survive, so too will the knowledge of group theory, and of linear algebra, and of computability theory.
From the point of view of anyone in 5000 CE or 10000 CE, it will seem absurdly short-sighted that someone in 2020 CE thought that the important thing about elliptic curves was that cryptography based on them permitted long-forgotten nations like Russia to achieve informatic independence from the long-forgotten United Nations of America, because they were not yet to discover the Elliptic Curve Discrete Log Algorithm for 440 more years, and didn't have large quantum computers yet.
I say that physics and computers are less insignificant than cryptography and finance because knowledge of physics does progressively improve, and is objective, like that of mathematics; and computers both serve to advance knowledge of mathematics, and are themselves imperfect realizations of abstract mathematical objects, what is often called automata theory. But certainly questions like how to get CUDA to run properly with a particular model of Tesla card, or which versions of Blink support Webfonts, are of no importance at all from the standpoint of 5000 CE or 10000 CE — but the Halting Problem will still be uncomputable, long after Turing's name is forgotten.
Physics theories, though, are historically contingent and provisional in a way that mathematical theories are not. The quantum theory of probability is, as Aaronson's book explains, an internally self-consistent extension of probability theory to the complex plane entirely apart from its use to describe the behavior of light, electrons and so on. Theorems can be proven within its axiomatic system, and those theorems will continue to hold even when the humans learn how it fails to describe the contingent reality of this universe. So, again, mathematics is eternal, at least until the libraries are burned, and exact; physics is a provisional approximation, until a better approximation is found.
Michelangelo painted it because it’s beautiful; but if you’re trying to figure out why someone financed it — it’s because the Medici’s gained significant reputation through such displays of wealth (in addition to personal enjoyment).
Mathematicians do mathematics because they find it transcendently beautiful — but if you’re asking why they’re allowed to spend billions a year doing that, the answer does involve all those applications delivering value to everyone else.
Your appreciation of that abstract beauty isn’t why everyone else pays, and honestly, isn’t necessarily a great reason for other people to pay you to do math.
When you’re making a sales pitch, talk about their needs.
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.
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.
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.
Mathematicians should make an effort to reach out to non-mathematicians because that category also includes people like, you know, physicists, engineers, computer scientists, students who may want to one day become mathematicians, those kinds of people.
The point about professions wasn't that mathematicians don't have the ability to do those things (although I'm quite certain most don't have the constitution to do many blue collar jobs), it was that if they were spending 40-50 hours a week collecting the town's garbage, working at a water treatment plant, or doing hot tar roofing, they would no longer have the time or energy to be doing math for a living.
You are truly delusional to think that funding is "only necessary to the extent that it helps keep the torch-wielding villagers away from the gate". Taxes collected from the people you seem to have so much contempt for (basically everyone) are what allow mathematicians to live in ivory towers doing research mathematics for a living. The patronage system of old (which allowed for people like Bruno and Gauss to get any education at all) was even worse, as the money they were receiving was the product of borderline or outright slavery.
Your bizarre characterization of mathematicians as saint-like figures levitating above the unwashed masses is indicative of a pretty poor understanding of history and a shocking lack of ability to empathize. I hope you understand that people who think like you (people who are disgusted by those who built and paid for the ivory towers in which your heroes reside) are the reason why people support things like defunding universities.
It's definitely not necessary to have taxes or a 21st-century-level GDP to do mathematics. Current world GDP is about US$17500 per capita PPP, three times the income I've been living on for years, and 1500 times the world GDP in the time of Archimedes. Computers do help, but they aren't essential, and most of the economy isn't devoted to producing computers or other mathematically useful goods anyway; most of it is devoted to things like the steak I just ate, tearing down buildings and putting them back up, killing people in senseless wars, destroying the atmosphere, team sports, junk food flavorings, surveillance capitalism like Facebook, literal prostitution, disposable fashion, toys, furniture, second cars, daytime TV, and so on.
Admittedly, a significant fraction of world GDP is devoted to essentials like child care, elder care, primary food production, housing, and education. But an enormous amount of it is just wasted and counterproductive effort.
However, you weren't talking about those parts; you were talking about truly essential services. Garbage collection and water treatment are essential but are not significant fractions of the GDP. Let's consider garbage collection, using US statistics. The US has 118520 garbage collectors, including the people who work at recycling plants and dumps, out of a population of 328 million people. If this difficult, dangerous, and sometimes unpleasant work were shared equitably among everyone, it would average 52 seconds per person per week, ¾ hour per year. In practice, even with good coordination, you'd probably lose an order of magnitude in efficiency to the lack of specialization, so probably sharing it equitably would mean that everyone would spend an hour or so every couple of months sorting the recycling at the recycling plant. This would have several salutary effects: people would learn not to put milk bottles in the recycling bin without rinsing them, the social stigma attached to garbage collection would disappear, and garbage collection contracts would no longer be an appealing way for mafias to dispose of clandestine murder victims' bodies.
As for construction work, although I'm not a journeyman electrician or anything, I've poured concrete a few times, I've bent and tied rebar, and I've repaired roofs; and when I was volunteering at the Casa de María in the slums near here, almost everybody I knew there had built their own house (or married or been born to someone who had.) With modern materials, you can build a perfectly adequate and livable house in a person-month, and it can house a family for several lifetimes. Even inefficient construction techniques like adobe, which I've also done, require less than a person-year per family dwelling. There is absolutely no need for people to specialize in hot-tar roofing as a career. That's senselessly exploitative oppression, and it destroys people's physical health as well as their intellectual potential.
Maybe you think that, if some people don't spend 40–50 hour weeks destroying their health breathing in construction dust, then other people will have to go homeless, because there won't be enough housing. The simple ratio I gave above should clarify why that isn't the case: one person-month of construction work per lifetime is more than enough to supply everyone with adequate housing, and that's even without 3-D printing in concrete to build new houses. The reason people go homeless is that they're not allowed to build houses, or the government bulldozes their houses (this happened to a group of my friends), or they're socially isolated and have sufficient mental or physical health problems that they can't take care of themselves.
In the US, about 3% of the population raises food full-time. If this labor were distributed across the population as a whole, it would amount to an hour or two per week. Gardening for an hour or two per week is not enough to seriously impact your mathematical productivity, whether you're driving a combine or tying tomato plants to the fence.
The big time commitments — which mathematicians often do end up doing — are child care, elder care, and education. The kibbutzim have shown that it's possible to collectivize these in a useful and humane way; school and nursing-home systems in places like the US have shown that it's possible to collectivize them in destructive and unbelievably cruel ways. The economy and government the non-mathematicians have constructed makes it very difficult to evade these curses, whether or not you are a mathematician.
As for slavery, slavery does not help education; not only is it inhumane and degrading to both the slave and the owner, it's an inefficient way to satisfy material needs. If the serfs had been liberated before Bruno (who had no patron) and Gauss were born, they would have had greater opportunities to educate themselves, not less.
You say that students of mathematics, physicists, engineers, and so on are "non-mathematicians". I'm not entirely in agreement with that but I'm willing to stipulate it for the sake of this conversation. I still don't think there's any reason for mathematicians to care about their opinion. If a student of mathematics thinks they have squared the circle or that differential forms are useless, [other] mathematicians have no reason to care, except that it might be a fun conversation with someone who might grow into a future collaborator, or that the conversation might sharpen their own understanding of differential forms or whatever. Students of mathematics, physicists, and engineers have motives of their own for caring about mathematics, though. I don't think [other] mathematicians have any responsibility for convincing them of that, nor any real benefit in doing so, except, again, insofar as it might result in interesting new mathematics. But if physicists by and large don't care about category theory (though I've met at least one exception), that doesn't really affect the category theorists, much less the consistency or beauty of category theory. Certainly category theorists wouldn't be doing themselves any favors by writing grants that pretend they're doing some kind of industrial R&D.
I don't think of mathematicians as saint-like figures levitating above the unwashed masses. I think of the unwashed masses as totally depraved screaming degraded chimpanzees throwing turds, and the mathematicians as slightly less depraved, screaming a bit less, slightly less degraded, but still basically chimpanzees.
> (By contrast, non-mathematicians are unable to build anything larger than a small hut without help from mathematicians in the form of geometry.)
If being a mathematician requires this sort of arrogant attitude, then I am all for locking those people up in an ivory tower and willingly foregoing the fruits of their labor.
The idea of applying mathematics and science to the efforts of people doing things instead of thinking about things is actually quite recent--maybe 300-ish years ago. Medieval Europeans didn't need a deep understanding of geometry or physics to discover flying buttresses or build Gothic cathedrals. Go back further in time and look at the majesty of Stonehenge or the Pyramids; the people who built those had no concept of tangents or pi and yet built what they did.
> I think the downvoting of my "tirade" to -2 has shown that non-mathematicians hate and fear mathematicians
No. I like mathematicians quite a lot, but I think you have your head stuck up your own ass.
You must be a barely educated American. Please, Mediterranean peoples had contact with basic Algebra and irrational numbers (and the Pi ratio) since millenia.
> Go back further in time and look at the majesty of Stonehenge or the Pyramids; the people who built those had no concept of tangents or pi and yet built what they did.
The Sumerians were doing geometry in 2450 BCE, and the Egyptians were in contact with them. Older Sumerian texts (from before 3100 BCE) don't have a lot of geometry but do contain numerical measurements and arithmetic used for accounting.
The Moscow Mathematical Papyrus, from Egypt, is from the 13th Dynasty (ended 1649 BCE), and it has a problem in it about the volume of the frustum of a pyramid. The Rhind Papyrus (around 1550 BCE) contains six problems about building pyramids, some problems about granary design, and a number of problems about real estate. The pyramids analyzed therein are building-sized. At this point the Egyptians had been building pyramids for a millennium, but no older mathematical texts have survived (aside from a diagram from 1000 years earlier showing how to measure off the slope of a mastaba), but few papyri last even the 4000 years of these papyri. Papyrus is fragile.
Nevertheless, it seems that the ancient Egyptians considered the knowledge of mathematics important to building pyramids, at least by the end of the pyramid-building period.
As for Stonehenge, we have no idea. The folks who built it didn't have a writing system, so we don't know much about how they thought. Still, it does seem pretty plausible that you could roll a big stone lintel up a hill of sand, or carefully balance it onto progressively higher stone pivots, without knowing the Pythagorean theorem. I guess Stonehenge is bigger than a small hut, so you've got me there.
There are Babylonian and Egyptian sources describing how to solve quadratic and some cubic equations from about 1600 BCE, but that is unfortunately at the end of the pyramid-building period. I think it's likely that they had this knowledge much earlier, but it's possible that they built the Pyramids, or most of them, before anyone had figured that out.
> 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.
Who is "a mathematician"? I definitely don't mean "someone with academic credentials or other official recognition"; surely Erdős was a mathematician when he was a teenager, Ramanujan was a mathematician before he wrote to Hardy, and Lagrange was a mathematician when he discovered the variational calculus with Euler; I think it's even reasonable to assert that Socrates was a mathematician when he taught Menon how to draw a line of length √½, because he demonstrated the correctness of the construction mathematically rather than just asserting it, even though he surely did not discover it at that moment. I think it's sufficient to be doing mathematics as an end in itself.
But that doesn't help much; what does it mean to be "doing mathematics"? Is it sufficient to read a proof? How about reconstructing a proof you vaguely remember? How about working some exercises in a textbook? Does it matter if the exercises are arithmetic or differential equations? What about when Martin Gardner rediscovered some well-known theorem or other? Might it even be sufficient to be doing mathematics for some other purpose, such as predicting the motions of the planets or the flight of an artillery shell, rather than an end in itself?
It seems that there's unavoidably a gray area; the toddler who counts "one, two, three, seven, ten" is definitely not "doing mathematics", while Scholze was surely "doing mathematics" when he discovered perfectoid spaces. Somewhere in between, there are cases where you can plausibly make an argument either way. (I don't think Ramanujan before his contact with Hardy is one of them, but perhaps that's self-serving bias on my part — I have no academic credentials of any kind, other than publications.)
But that's okay. Language isn't math, so we can't expect people to come to a perfect consensus about what it means, although we can of course attempt to clarify our thinking, however much the non-mathematicians may detest and attempt to sabotage such activity.
So, what do you think is a good definition of "a mathematician"?
> So, what do you think is a good definition of "a mathematician"?
It depends on the context. The definition I'd like to advance is that a mathematician is someone who does mathematics (and that what one usually means by "a mathematician" is something more like "one who habitually does mathematics, or one whose profession is the doing of mathematics"); the toddler, while counting "one, two, three", is a mathematician, who may turn into a new-language learner when continuing "seven, ten", or may still be a mathematician if that toddler is fascinated by and exploring number patterns. By this definition, almost everyone is a mathematician at some time or other, so that making claims about what the population of mathematicians does is little more than making claims about what everyone does.
There are at least two problems with this definition: (1) it shifts the question from "who is a mathematician?" to "what is doing mathematics?"; and (2) it blurs meaningful distinctions between people who are habitual or professional mathematicians, among amateurs, dabblers, and tyros, and other distinctions that one might want to make. My answer to (1) is that I would give an equally broad answer to the latter question, and my answers to (2) are twofold, namely (a) tough, and (b) the distinctions can be preserved by including additional modifiers, as I have done. This resolves these problems to my satisfaction, but I don't expect them to satisfy everyone, or even many.
> I don't think Ramanujan before his contact with Hardy is one of them, but perhaps that's self-serving bias on my part — I have no academic credentials of any kind, other than publications.
That sounds self-defeating, rather than self-serving! Why not recognise Ramanujan as a mathematician before Hardy? Surely the same genius was there, just not expressed in familiar ways; so what Hardy can be said to have done to Ramanujan is surely not to have turned him into a mathematician, but instead to have taught him the common language of mathematics in which to express what he already knew but couldn't fully communicate to others.
I didn't mean to assert that young Ramanujan was clearly not a mathematician — rather the opposite!
Perhaps in practice my definition of "a mathematician" is "someone who, when wrong, responds to disagreement by changing their mind rather than becoming defensive or downvoting you", an event I see on a daily basis in lectures on mathematics and very rarely outside of them.
> Perhaps in practice my definition of "a mathematician" is "someone who, when wrong, responds to disagreement by changing their mind rather than becoming defensive or downvoting you", an event I see on a daily basis in lectures on mathematics and very rarely outside of them.
Mathematicians are often OK at this within their discipline, but we're as bad as anyone else at it when dealing with human affairs. (At least, I am.) I might rather suggest the less flattering characterisation of a mathematician who will argue with a statement with which they agree, just to see if it breaks. (At least, I do.)
> Mathematicians are perfectly capable of doing all those self-care things, as monks do in every monastery
Are they, though? In the pursuit of my PhD, I met plenty of mathematicians who could barely wipe their own ass, let alone cook a meal or, god forbid, build a simple hut. Did you know that most mathematicians use computers? Do you expect these same people to manage the chemistry, physics, engineering, mining and logistics necessary to build their own computing devices?
> 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.
That's quite a chain of conjectures... you may be a mathematician, but you certainly aren't holding yourself to mathematical standards here.
Here's a counterexample. I downvoted you. I'm a mathematician. And fwiw Galois died in a duel, which is, by definition, a consensual affair. His killing was an unreasonable, unjustified tragedy, but he brought it on himself. Oded Schramm did himself on a mountain; by the way -- you're shit-talking "non-mathematicians" for taking senseless risks, but missing the obvious and playing victim while referring to non-mathematicians as "torch-wielding villagers."
I downvoted you for your insufferable superiority complex and mindboggling narrow-mindedness.
You seem to be under the misconception that I am a mathematician. I think that's a bit of a stretch of the term, although I do enjoy math; as far as I know, I've never published or discovered a single novel mathematical result, and I certainly don't have any academic mathematical credentials. Very few of the humans would call me a mathematician.
Everyone is born incapable of carrying out self-care tasks. Some of us remain that way for our entire lives, but most don't. I haven't observed a strong correlation between mathematical ability and potty-training or cooking ability, so surely any community of mathematicians would have enough people who could cook a meal that they'd get along okay, in the improbable scenario where they were forced into strict autarky.
Duels are not consensual except in the sense that it's consensual to surrender to the police when they tackle you. Struggling against the police, or fleeing the duel, is overwhelmingly likely to get you killed.
I'm not sure where you're getting this idea that I'm "shit-talking non-mathematicians for taking senseless risks"; one mathematician I know went to Italy for a week to stay in the house of a man she'd just met in Argentina to dance in his tango show, while another juggled his baby to illustrate a lecture about siteswaps (and, perhaps more shockingly, gave up tenure for the baby's mother). I think mathematicians tend to take more long-term risks and less short-term risks than non-mathematicians. None of those examples is quite in the same category as "he grabbed the cop by her bulletproof vest", for example, which is something I saw a non-mathematician do as I helped the cops to arrest him.
What I'm shit-talking non-mathematicians for is killing mathematicians, burning the Academy and the works of the Mohists, destroying the German universities in the service of a stupid self-congratulatory racist ideology, and destroying democracy in America for the same reason. None of those amount to "taking senseless risks"; their undesirable results were nearly guaranteed and indeed intended by the perpetrators.
You're not wrong about the insufferable superiority complex, but you ought to consider the way in which my "tirade" is actually correct, even if my insufferable superiority complex annoys you. As a mathematician, you undoubtedly have a great deal of experience changing your mind after hearing arguments from people you don't particularly like. I suggest you try doing it in this case.
> Duels are not consensual except in the sense that it's consensual to surrender to the police when they tackle you. Struggling against the police, or fleeing the duel, is overwhelmingly likely to get you killed.
The history is quite unclear with regard to the fateful duel of Galois, and historical record suggests that it's quite possible he was the one who laid the challenge!
> As a mathematician, you undoubtedly have a great deal of experience changing your mind after hearing arguments from people you don't particularly like. I suggest you try doing it in this case.
I admit that I'm wrong when it's demonstrated that I'm wrong. This is common among mathematicians, and makes me insufferable in my own way. I would suggest you reconsider your characterization of the downvotes you've received -- multiple mathematicians are responding to you, and there's lots of us here on HN: your audience is not comprised of torch-wielding villagers. And yet you continue to dig in -- this sort of conversation is undesirable here, and I'd recommend you to consider the site guidelines and your fellow conversational partners' opinions before continuing. (I'll desist after this comment, and bid you farewell)
> Duels are not consensual except in the sense that it's consensual to surrender to the police when they tackle you. Struggling against the police, or fleeing the duel, is overwhelmingly likely to get you killed.
That's not how duels work. A challenge for a duel is usually issued in response to a perceived insult or injury to one's honor, and the request for a duel would often be delivered in writing. The only penalty for refusing a duel is the attendant impact on social standing--you could be seen as dishonorable or cowardly for refusing a duel. And even if you agreed to a duel, you might be able to get out of it simply by being disagreeable as to the actual conditions of a duel.
Listen, I don't know if you've ever lived in an honor society, but if you're a man in an honor society, "you could be seen as dishonorable or cowardly" (the word they used for me here was puto, which means "faggot") is pretty much a death sentence. Your understanding of comparative anthropology seems to be as weak as your understanding of ancient Egyptian mathematics.
That definitely was not a thing I had in mind, no, although I'm sure it has cast a shadow over the particular flavors of honor society I've had the displeasure of being subjected to — thanks to Hollywood, if nothing else.
My comment above, in a text color that's easier to read:
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.
And the part below, which apparently people also want to silence:
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 [outdated: now -4] 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.
> 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 ), 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
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.
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.
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.
Rigor means not hand-waving about things that a skeptic might doubt, not skipping corner cases, etc.
Formal means doing things like a computer -- strictly symbolic analysis that doesn't claim to do the impossible task accurately map back to our informal ideas of what things mean.
Formality is across a chasm -- it's the most accurate kind of math we can do, but it can't be trusted to say that a formal proof about say complex numbers actually applies to what you are thinking about when you day "complex numbers".
As is said, "It is impossible to pass from the informal by purely formal means."
Here's a better explanation: https://www.quora.com/What-is-difference-between-rigorous-an...
The less rigorously the arrangement (and proofed) , the more likely the outcome is wrong though the syntax (symbol manipulation) is correct.
Hope that sums it up in my understanding :)
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.
Link list of the discussion threads: https://owlofminerva.net/kubota/update-to-the-foundations-of...
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.
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.
https://news.ycombinator.com/item?id=20909404
Here is the main site. http://us.metamath.org/index.html
Here is the book which can help with understanding. 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=PL1jSu6GGefBm7RBP0Id2S...
it can be found here, 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
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
Fascinating stuff explained in just over a thousand pages.
It's hardly a new thing. David Hestenes has been writing books about its advantages in physics since the 1960's.
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.
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.
I’d also accept an example of knowledge you don’t believe is expressible in mathematics.
It's true that we only have cryptography, computers, physics, and finance — and not only the modern kind — because of the human study of mathematics. But cryptography and finance are of distinctly tertiary importance, computers and physics of secondary importance, and mathematics of primary importance. So it is nonsense to say that mathematics is important because it helps us understand physics. Mathematics is important because it transcends physics; the same mathematical theories would be consistent in a universe with totally different physics. Their beauty does not depend on whether or not they happen to describe the physics in a particular universe or not.
The Pythagorean Theorem was discovered by the humans in Mesopotamia somewhere between 3500 and 5000 years ago; nobody knows who discovered it. (Pythagoras wouldn't be born for centuries.) It was used to design buildings, but the buildings have been worn to dust. It was used then to divide up farmland, but the farmers are dead, their bones have worn away to dust in the sand, their names are mostly forgotten, and their farmland turned to desert. But the knowledge of the theorem, and the place-value number system the Babylonians invented, has endured, and the humans still divide the circle into 360 degrees, each degree into 60 minutes, and each minute into 60 seconds, a tradition inherited from the Babylonians.
Moreover, the stars and planets have moved in a way described by the Pythagorean Theorem since there have been planets and stars, for almost 14 billion of the time unit that would eventually be a "year" on Earth. And, most likely, they will continue to do so for as long as there are planets and stars; and as long as there are humans, they will know the Pythagorean Theorem, even if the name of Babylon is forgotten.
Today the humans consider cryptography important because it governs the rise and fall of nations and empires; they consider finance important because it governs the rise and fall of firms, and decides which humans are powerful and which humans are poor and starving. But, it is nearly certain that all of those powerful humans will be dead in a century and a half, and all of those nations and empires will be gone in a millennium.
But, if libraries survive, so too will the knowledge of group theory, and of linear algebra, and of computability theory.
From the point of view of anyone in 5000 CE or 10000 CE, it will seem absurdly short-sighted that someone in 2020 CE thought that the important thing about elliptic curves was that cryptography based on them permitted long-forgotten nations like Russia to achieve informatic independence from the long-forgotten United Nations of America, because they were not yet to discover the Elliptic Curve Discrete Log Algorithm for 440 more years, and didn't have large quantum computers yet.
I say that physics and computers are less insignificant than cryptography and finance because knowledge of physics does progressively improve, and is objective, like that of mathematics; and computers both serve to advance knowledge of mathematics, and are themselves imperfect realizations of abstract mathematical objects, what is often called automata theory. But certainly questions like how to get CUDA to run properly with a particular model of Tesla card, or which versions of Blink support Webfonts, are of no importance at all from the standpoint of 5000 CE or 10000 CE — but the Halting Problem will still be uncomputable, long after Turing's name is forgotten.
Physics theories, though, are historically contingent and provisional in a way that mathematical theories are not. The quantum theory of probability is, as Aaronson's book explains, an internally self-consistent extension of probability theory to the complex plane entirely apart from its use to describe the behavior of light, electrons and so on. Theorems can be proven within its axiomatic system, and those theorems will continue to hold even when the humans learn how it fails to describe the contingent reality of this universe. So, again, mathematics is eternal, at least until the libraries are burned, and exact; physics is a provisional approximation, until a better approximation is found.
(For a much more cynical perspective on the humans, see https://news.ycombinator.com/item?id=22393163.)
Mathematicians do mathematics because they find it transcendently beautiful — but if you’re asking why they’re allowed to spend billions a year doing that, the answer does involve all those applications delivering value to everyone else.
Your appreciation of that abstract beauty isn’t why everyone else pays, and honestly, isn’t necessarily a great reason for other people to pay you to do math.
When you’re making a sales pitch, talk about their needs.
Why should anyone care about anything?
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.
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.
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.
The point about professions wasn't that mathematicians don't have the ability to do those things (although I'm quite certain most don't have the constitution to do many blue collar jobs), it was that if they were spending 40-50 hours a week collecting the town's garbage, working at a water treatment plant, or doing hot tar roofing, they would no longer have the time or energy to be doing math for a living.
You are truly delusional to think that funding is "only necessary to the extent that it helps keep the torch-wielding villagers away from the gate". Taxes collected from the people you seem to have so much contempt for (basically everyone) are what allow mathematicians to live in ivory towers doing research mathematics for a living. The patronage system of old (which allowed for people like Bruno and Gauss to get any education at all) was even worse, as the money they were receiving was the product of borderline or outright slavery. Your bizarre characterization of mathematicians as saint-like figures levitating above the unwashed masses is indicative of a pretty poor understanding of history and a shocking lack of ability to empathize. I hope you understand that people who think like you (people who are disgusted by those who built and paid for the ivory towers in which your heroes reside) are the reason why people support things like defunding universities.
Admittedly, a significant fraction of world GDP is devoted to essentials like child care, elder care, primary food production, housing, and education. But an enormous amount of it is just wasted and counterproductive effort.
However, you weren't talking about those parts; you were talking about truly essential services. Garbage collection and water treatment are essential but are not significant fractions of the GDP. Let's consider garbage collection, using US statistics. The US has 118520 garbage collectors, including the people who work at recycling plants and dumps, out of a population of 328 million people. If this difficult, dangerous, and sometimes unpleasant work were shared equitably among everyone, it would average 52 seconds per person per week, ¾ hour per year. In practice, even with good coordination, you'd probably lose an order of magnitude in efficiency to the lack of specialization, so probably sharing it equitably would mean that everyone would spend an hour or so every couple of months sorting the recycling at the recycling plant. This would have several salutary effects: people would learn not to put milk bottles in the recycling bin without rinsing them, the social stigma attached to garbage collection would disappear, and garbage collection contracts would no longer be an appealing way for mafias to dispose of clandestine murder victims' bodies.
As for construction work, although I'm not a journeyman electrician or anything, I've poured concrete a few times, I've bent and tied rebar, and I've repaired roofs; and when I was volunteering at the Casa de María in the slums near here, almost everybody I knew there had built their own house (or married or been born to someone who had.) With modern materials, you can build a perfectly adequate and livable house in a person-month, and it can house a family for several lifetimes. Even inefficient construction techniques like adobe, which I've also done, require less than a person-year per family dwelling. There is absolutely no need for people to specialize in hot-tar roofing as a career. That's senselessly exploitative oppression, and it destroys people's physical health as well as their intellectual potential.
Maybe you think that, if some people don't spend 40–50 hour weeks destroying their health breathing in construction dust, then other people will have to go homeless, because there won't be enough housing. The simple ratio I gave above should clarify why that isn't the case: one person-month of construction work per lifetime is more than enough to supply everyone with adequate housing, and that's even without 3-D printing in concrete to build new houses. The reason people go homeless is that they're not allowed to build houses, or the government bulldozes their houses (this happened to a group of my friends), or they're socially isolated and have sufficient mental or physical health problems that they can't take care of themselves.
In the US, about 3% of the population raises food full-time. If this labor were distributed across the population as a whole, it would amount to an hour or two per week. Gardening for an hour or two per week is not enough to seriously impact your mathematical productivity, whether you're driving a combine or tying tomato plants to the fence.
The big time commitments — which mathematicians often do end up doing — are child care, elder care, and education. The kibbutzim have shown that it's possible to collectivize these in a useful and humane way; school and nursing-home systems in places like the US have shown that it's possible to collectivize them in destructive and unbelievably cruel ways. The economy and government the non-mathematicians have constructed makes it very difficult to evade these curses, whether or not you are a mathematician.
As for slavery, slavery does not help education; not only is it inhumane and degrading to both the slave and the owner, it's an inefficient way to satisfy material needs. If the serfs had been liberated before Bruno (who had no patron) and Gauss were born, they would have had greater opportunities to educate themselves, not less.
You say that students of mathematics, physicists, engineers, and so on are "non-mathematicians". I'm not entirely in agreement with that but I'm willing to stipulate it for the sake of this conversation. I still don't think there's any reason for mathematicians to care about their opinion. If a student of mathematics thinks they have squared the circle or that differential forms are useless, [other] mathematicians have no reason to care, except that it might be a fun conversation with someone who might grow into a future collaborator, or that the conversation might sharpen their own understanding of differential forms or whatever. Students of mathematics, physicists, and engineers have motives of their own for caring about mathematics, though. I don't think [other] mathematicians have any responsibility for convincing them of that, nor any real benefit in doing so, except, again, insofar as it might result in interesting new mathematics. But if physicists by and large don't care about category theory (though I've met at least one exception), that doesn't really affect the category theorists, much less the consistency or beauty of category theory. Certainly category theorists wouldn't be doing themselves any favors by writing grants that pretend they're doing some kind of industrial R&D.
I don't think of mathematicians as saint-like figures levitating above the unwashed masses. I think of the unwashed masses as totally depraved screaming degraded chimpanzees throwing turds, and the mathematicians as slightly less depraved, screaming a bit less, slightly less degraded, but still basically chimpanzees.
If being a mathematician requires this sort of arrogant attitude, then I am all for locking those people up in an ivory tower and willingly foregoing the fruits of their labor.
The idea of applying mathematics and science to the efforts of people doing things instead of thinking about things is actually quite recent--maybe 300-ish years ago. Medieval Europeans didn't need a deep understanding of geometry or physics to discover flying buttresses or build Gothic cathedrals. Go back further in time and look at the majesty of Stonehenge or the Pyramids; the people who built those had no concept of tangents or pi and yet built what they did.
> I think the downvoting of my "tirade" to -2 has shown that non-mathematicians hate and fear mathematicians
No. I like mathematicians quite a lot, but I think you have your head stuck up your own ass.
> Go back further in time and look at the majesty of Stonehenge or the Pyramids; the people who built those had no concept of tangents or pi and yet built what they did.
The Sumerians were doing geometry in 2450 BCE, and the Egyptians were in contact with them. Older Sumerian texts (from before 3100 BCE) don't have a lot of geometry but do contain numerical measurements and arithmetic used for accounting.
The Moscow Mathematical Papyrus, from Egypt, is from the 13th Dynasty (ended 1649 BCE), and it has a problem in it about the volume of the frustum of a pyramid. The Rhind Papyrus (around 1550 BCE) contains six problems about building pyramids, some problems about granary design, and a number of problems about real estate. The pyramids analyzed therein are building-sized. At this point the Egyptians had been building pyramids for a millennium, but no older mathematical texts have survived (aside from a diagram from 1000 years earlier showing how to measure off the slope of a mastaba), but few papyri last even the 4000 years of these papyri. Papyrus is fragile.
Nevertheless, it seems that the ancient Egyptians considered the knowledge of mathematics important to building pyramids, at least by the end of the pyramid-building period.
As for Stonehenge, we have no idea. The folks who built it didn't have a writing system, so we don't know much about how they thought. Still, it does seem pretty plausible that you could roll a big stone lintel up a hill of sand, or carefully balance it onto progressively higher stone pivots, without knowing the Pythagorean theorem. I guess Stonehenge is bigger than a small hut, so you've got me there.
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.
Who is "a mathematician"? I definitely don't mean "someone with academic credentials or other official recognition"; surely Erdős was a mathematician when he was a teenager, Ramanujan was a mathematician before he wrote to Hardy, and Lagrange was a mathematician when he discovered the variational calculus with Euler; I think it's even reasonable to assert that Socrates was a mathematician when he taught Menon how to draw a line of length √½, because he demonstrated the correctness of the construction mathematically rather than just asserting it, even though he surely did not discover it at that moment. I think it's sufficient to be doing mathematics as an end in itself.
But that doesn't help much; what does it mean to be "doing mathematics"? Is it sufficient to read a proof? How about reconstructing a proof you vaguely remember? How about working some exercises in a textbook? Does it matter if the exercises are arithmetic or differential equations? What about when Martin Gardner rediscovered some well-known theorem or other? Might it even be sufficient to be doing mathematics for some other purpose, such as predicting the motions of the planets or the flight of an artillery shell, rather than an end in itself?
It seems that there's unavoidably a gray area; the toddler who counts "one, two, three, seven, ten" is definitely not "doing mathematics", while Scholze was surely "doing mathematics" when he discovered perfectoid spaces. Somewhere in between, there are cases where you can plausibly make an argument either way. (I don't think Ramanujan before his contact with Hardy is one of them, but perhaps that's self-serving bias on my part — I have no academic credentials of any kind, other than publications.)
But that's okay. Language isn't math, so we can't expect people to come to a perfect consensus about what it means, although we can of course attempt to clarify our thinking, however much the non-mathematicians may detest and attempt to sabotage such activity.
So, what do you think is a good definition of "a mathematician"?
It depends on the context. The definition I'd like to advance is that a mathematician is someone who does mathematics (and that what one usually means by "a mathematician" is something more like "one who habitually does mathematics, or one whose profession is the doing of mathematics"); the toddler, while counting "one, two, three", is a mathematician, who may turn into a new-language learner when continuing "seven, ten", or may still be a mathematician if that toddler is fascinated by and exploring number patterns. By this definition, almost everyone is a mathematician at some time or other, so that making claims about what the population of mathematicians does is little more than making claims about what everyone does.
There are at least two problems with this definition: (1) it shifts the question from "who is a mathematician?" to "what is doing mathematics?"; and (2) it blurs meaningful distinctions between people who are habitual or professional mathematicians, among amateurs, dabblers, and tyros, and other distinctions that one might want to make. My answer to (1) is that I would give an equally broad answer to the latter question, and my answers to (2) are twofold, namely (a) tough, and (b) the distinctions can be preserved by including additional modifiers, as I have done. This resolves these problems to my satisfaction, but I don't expect them to satisfy everyone, or even many.
> I don't think Ramanujan before his contact with Hardy is one of them, but perhaps that's self-serving bias on my part — I have no academic credentials of any kind, other than publications.
That sounds self-defeating, rather than self-serving! Why not recognise Ramanujan as a mathematician before Hardy? Surely the same genius was there, just not expressed in familiar ways; so what Hardy can be said to have done to Ramanujan is surely not to have turned him into a mathematician, but instead to have taught him the common language of mathematics in which to express what he already knew but couldn't fully communicate to others.
Perhaps in practice my definition of "a mathematician" is "someone who, when wrong, responds to disagreement by changing their mind rather than becoming defensive or downvoting you", an event I see on a daily basis in lectures on mathematics and very rarely outside of them.
Mathematicians are often OK at this within their discipline, but we're as bad as anyone else at it when dealing with human affairs. (At least, I am.) I might rather suggest the less flattering characterisation of a mathematician who will argue with a statement with which they agree, just to see if it breaks. (At least, I do.)
I've heard worse suggestions. I assume the trains will at least run on time. Will the budget get balanced, that's another question.
If we weld the doors shut, the scheduling will be iron-clad!
Are they, though? In the pursuit of my PhD, I met plenty of mathematicians who could barely wipe their own ass, let alone cook a meal or, god forbid, build a simple hut. Did you know that most mathematicians use computers? Do you expect these same people to manage the chemistry, physics, engineering, mining and logistics necessary to build their own computing devices?
> 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.
That's quite a chain of conjectures... you may be a mathematician, but you certainly aren't holding yourself to mathematical standards here.
Here's a counterexample. I downvoted you. I'm a mathematician. And fwiw Galois died in a duel, which is, by definition, a consensual affair. His killing was an unreasonable, unjustified tragedy, but he brought it on himself. Oded Schramm did himself on a mountain; by the way -- you're shit-talking "non-mathematicians" for taking senseless risks, but missing the obvious and playing victim while referring to non-mathematicians as "torch-wielding villagers."
I downvoted you for your insufferable superiority complex and mindboggling narrow-mindedness.
Everyone is born incapable of carrying out self-care tasks. Some of us remain that way for our entire lives, but most don't. I haven't observed a strong correlation between mathematical ability and potty-training or cooking ability, so surely any community of mathematicians would have enough people who could cook a meal that they'd get along okay, in the improbable scenario where they were forced into strict autarky.
Duels are not consensual except in the sense that it's consensual to surrender to the police when they tackle you. Struggling against the police, or fleeing the duel, is overwhelmingly likely to get you killed.
I'm not sure where you're getting this idea that I'm "shit-talking non-mathematicians for taking senseless risks"; one mathematician I know went to Italy for a week to stay in the house of a man she'd just met in Argentina to dance in his tango show, while another juggled his baby to illustrate a lecture about siteswaps (and, perhaps more shockingly, gave up tenure for the baby's mother). I think mathematicians tend to take more long-term risks and less short-term risks than non-mathematicians. None of those examples is quite in the same category as "he grabbed the cop by her bulletproof vest", for example, which is something I saw a non-mathematician do as I helped the cops to arrest him.
What I'm shit-talking non-mathematicians for is killing mathematicians, burning the Academy and the works of the Mohists, destroying the German universities in the service of a stupid self-congratulatory racist ideology, and destroying democracy in America for the same reason. None of those amount to "taking senseless risks"; their undesirable results were nearly guaranteed and indeed intended by the perpetrators.
You're not wrong about the insufferable superiority complex, but you ought to consider the way in which my "tirade" is actually correct, even if my insufferable superiority complex annoys you. As a mathematician, you undoubtedly have a great deal of experience changing your mind after hearing arguments from people you don't particularly like. I suggest you try doing it in this case.
The history is quite unclear with regard to the fateful duel of Galois, and historical record suggests that it's quite possible he was the one who laid the challenge!
> As a mathematician, you undoubtedly have a great deal of experience changing your mind after hearing arguments from people you don't particularly like. I suggest you try doing it in this case.
I admit that I'm wrong when it's demonstrated that I'm wrong. This is common among mathematicians, and makes me insufferable in my own way. I would suggest you reconsider your characterization of the downvotes you've received -- multiple mathematicians are responding to you, and there's lots of us here on HN: your audience is not comprised of torch-wielding villagers. And yet you continue to dig in -- this sort of conversation is undesirable here, and I'd recommend you to consider the site guidelines and your fellow conversational partners' opinions before continuing. (I'll desist after this comment, and bid you farewell)
That's not how duels work. A challenge for a duel is usually issued in response to a perceived insult or injury to one's honor, and the request for a duel would often be delivered in writing. The only penalty for refusing a duel is the attendant impact on social standing--you could be seen as dishonorable or cowardly for refusing a duel. And even if you agreed to a duel, you might be able to get out of it simply by being disagreeable as to the actual conditions of a duel.
You seem to be using a "Wild West" context for "duel", which (while relatively recent) is a very narrow window, historically speaking.
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.
And the part below, which apparently people also want to silence:
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 [outdated: now -4] 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.