Where is the fashionable mathematics?(xenaproject.wordpress.com)
xenaproject.wordpress.com
Where is the fashionable mathematics?
https://xenaproject.wordpress.com/2020/02/09/where-is-the-fashionable-mathematics/
72 comments
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.
It's sure going to be interesting, though.
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.
One of these questions I never dared to ask; What does formal mean in the area of mathematics? Is it like finalizing a formula / proof?
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.
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.
That's not quite right.
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...
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...
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.
Thank you, that clears it up further. I recently saw the movie “the man who knew infinity” and so it got me thinking about this meta questions.
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.
Hope that sums it up in my understanding :)
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 :)
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.
[deleted]
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.
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.
My comment on Kevin Buzzard's intervention:
https://groups.google.com/d/msg/metamath/Fgn0qZEzCko/bvVem1B...
Link list of the discussion threads: https://owlofminerva.net/kubota/update-to-the-foundations-of...
Link list of the discussion threads: https://owlofminerva.net/kubota/update-to-the-foundations-of...
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.
What would the better ergonomics look like? Do you have an idea what might be wrong with the theory?
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.
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.
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.
Related from last year: https://news.ycombinator.com/item?id=21200721
https://news.ycombinator.com/item?id=20909404
https://news.ycombinator.com/item?id=20909404
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?
I've been finding it useful to audit university classes. Do you have a university nearby?
If you can program you might like Metamath, it feels quite a lot like writing code.
Here is the main site. http://us.metamath.org/index.html
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
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
An article about fashionable mathematics and no mention of category theory?
Here: https://ncatlab.org/nlab/show/Higher+Algebra
Fascinating stuff explained in just over a thousand pages.
Fascinating stuff explained in just over a thousand pages.
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.
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.
Looks like Geometric Algebra is something that has been talked about quite a lot lately. (It is "vector algebra done right.")
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.
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.
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.
Mathematics is modern ontology.
We’re not great at predicting which parts of ontology are eventually useful in other fields — mostly physics and other hard science, but more recently computer science, economics + finance, and even things like sociology and linguistics.
So we let the people who self-select to be ontologists guide what the field researches — and this has generally been fairly effective. Certainly more effective than if we’d only looked at things which had immediate, obvious use. Complex numbers, widely used in science and engineering, were once regarded as suspect abstract nonsense. That’s why they’re called “imaginary numbers”: it was a pejorative name that stuck.
We have cryptography, computers, modern physics, and modern finance to show for our efforts, among other things.
It simply takes time (like, decades to centuries) for new ontological ideas to propagate to other fields. We’re hoping that formalizing into HoTT and other computer friendly systems will allow us to align with software development, and speed the process up.
That seems to be going well, and at an accelerating pace.
The hope is that HoTT and category theory give us a framework to do exactly what you propose — more easily specify and interlink knowledge.
Expect results around 2050.
It took around 40-60 years for category theory to have a big impact — but now it is in fields as far away from mathematics as linguistics. Hopefully HoTT will get there a little faster, but it’s still going to take decades to go from niche research to widely used in mathematics to widely used across disciplines.
So, to summarize:
1. Because we’re bad at predicting the future and abstract math has often turned out to be useful later.
2. Mathematics is trying to do exactly what you propose with knowledge, via exactly the programs this blog is talking about.
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 disagree that all knowledge, or even the most important items of knoknowledge, are reducible to mathematics.
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.
(For a much more cynical perspective on the humans, see https://news.ycombinator.com/item?id=22393163.)
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.)
It's quite ironic. Imaginary numbers are quite real, but real numbers are quite imaginary.
kragen(2)
> 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.