Opinion 1: Doron Zeilberger is a great mathematician and prophet of the computer-aided future, but he is still blinded by the idea that intrinsic value in mathematics comes from interestingness

John Carlos Baez

Mon Aug 28 2023

I agree with you that mathematical results should not be valued in proportion to the difficulty of their proofs. There are probably many things that make for a good result. But I especially like results that illuminate the world - that help us see things more clearly - and often these become more illuminating as we make their proofs simpler, because the illumination comes not just from knowing that the result is true, but why. So I am always trying to make everything simpler.

On another note, it would be good to see some examples of what you call “ridiculous ego-driven symbol pushing” in mathematics. Of course it is socially risky to name and shame, for several reasons! But I am a bit curious about what exactly you mean. Different people have quite different opinions about which mathematics is worthwhile and which is more symbol pushing. I find that as I learn more math, my opinion sometimes changes. So maybe we could chat about this offline sometime.

Owen Lynch

Mon Aug 28 2023

Part of that was just channeling the style of Dr. Z for the bit of this post. But more generally, I don’t think I’m in a position to be sure that different parts of math are worthless, because math can have surprising consequences down the line. Time and time again, parts of math which seem worthless on the outside have some hidden gem inside.

That being said, I do believe that much math is not pursued in the spirit of service to the scientist and engineer; it is pursued out of an intrinsic love for patterns. And the danger there is in the absence of “objective” criteria for what patterns are “interesting”, there is a tendency to equate interestingness with “sport-like” cleverness.

But it’s complicated, because often the most useful results are discovered only through “play”, using only “what seems interesting” as a guide!

With all that out of the way, I will be brave enough to name in public some parts of math that are valued within mainstream academia but not in my estimation.

1. Computing homotopy groups of the sphere.
2. Classifying finite groups.
3. The twin prime conjecture.
4. The general approach to mathematical statistical mechanics that I encountered in my master’s program, where there was a lot of attention paid to computing difficult partition functions by hand and phase transition, and not a lot of attention paid to fundamental issues like “what is an open system.” I’d prefer a “Zeilberger”-style treatment, where you just numerically investigate phase transition of different models, because this scales to more complex real-world situations where clever tricks don’t apply.
5. Anything to do with large cardinals.

There are other things that I have a suspicion aren’t that useful, but it could just be that I don’t know enough about them yet.

But of course, always happy to chat offline as well.

John Carlos Baez

Tue Aug 29 2023

At the end of your list you say you suspect items 1-5 aren’t useful. Of course ‘useful’ always begs the question: “useful for what?”. But somehow you changed the issue from “worthwhile” to “useful”. I don’t think math needs to be “useful” to be worthwhile.

For example, we probably know enough homotopy groups of spheres to do everything we currently need to do in math and physics. \pi_3(S^2)= \mathbb{Z} is important for skyrmions (topological solitons used to model baryons) . \pi_3(S^3) = \mathbb{Z} is important for instantons in SU(2) gauge theory (which cause detectable effects in the Standard Model). I’d say these are actually useful.

Very few people work on simply grinding out more higher homotopy groups of spheres. Most people who think about them are interested in they relate to other topics.

To category theorists, higher homotopy groups of spheres are interesting because they automatically arise when we repeatedly categorify the notion of “integer”. Joyal said “the sphere spectrum is the true integers”, and I explained that in week102 of This Week’s Finds. It’s really quite amazing!

There are also lots of shocking connections between homotopy groups of spheres and other subjects. Most famously, \lim_{n \to \infty} \pi_{n+3}(S^n) = \mathbb{Z}/24 has important connections to the huge network of ideas surrounding the number 24 which I overviewed in my recent lecture. It’s connected to how the double cover of the rotational symmetry group of the tetrahedron has 24 elements, the fact that bosonic string theory only works in 24+2-dimensional spacetime, the fact that superstring theory involves a 24-component field on the string worldsheet, the Riemann zeta function having \zeta(-1) = -1/12, the fact that at most 24 balls can touch a single ball of the same radius, the appearance of the number 24 in the formula for the discriminant of elliptic curves, and more.

And all this stuff about the number 24 is just a special case - admittedly, the most exciting special case - of the amazing relation between homotopy groups of spheres, Bernoulli numbers, the Riemann zeta function, the algebraic K-groups of the integers, and many other things that you might at first think were unconnected. I talked about the next case here: we have \lim_{n \to \infty} \pi_{n+7}(S^n) = \mathbb{Z}/240, and this is connected to how you can get at most 240 balls to touch a single ball of the same radius in 8 dimensions!

I wouldn’t go so far as to say most of this stuff is “useful”, but to me it’s worthwhile in very much the same way as the music of Bach: intricately patterned, surprising, endlessly mysterious, yet somehow inevitable. Unlike the music of Bach, this stuff emerges inevitably out of the fabric of mathematics itself.

It think it’s dangerous to lose oneself in these things. There are too many practical problems that need our attention. But I think that’s quite different from saying these things are “worthless”. In fact, it’s their bewitching fascination that makes them dangerous!

The question of how much math is “ego-driven” is fascinating to me. Certainly I get some egotistical pleasure in parading my knowledge as I just did. I try to keep it under control and focus on sharing the joy rather than merely showing off. It’s an endless challenge.

But I don’t think math is particularly ego-driven. I think almost any career path favored by ambitious men has an element of ego in it - and law, politics, business, sports, and practical forms of science are probably more ego-driven than math, simply because more people will be watching when you triumph. Frankly, nobody gives a damn when you prove \pi_{22}(S^{3}) = \mathbb{Z}/132 \times \mathbb{Z}/2. To work out something like that, which is apparently very hard, you have to be into the solitary pleasure of it.

Benjamin Bumpus

Tue Aug 29 2023

I think that, similarly to generalized discussions about what counts as “applied” mathematics, trying to define what “worthwhile” mathematics is and attempting to distinguish it from “symbol pushing” is itself not a useful activity. Grossly oversimplifying, scientific fields are determined by the questions that are asked and the methods employed and the communities involved. I believe that virtually all of us work on things that we believe are worthwhile and useful. As you both point out, we often learn some of the deepest, most “useful” notions through playing or by investigating seemingly useless notions. I guess that what I’m trying to say is: as long as we all ask ourselves what “worthwhile” means to us personally (so that we can work towards something which we consider to have substance) then we should not spend any time trying to determine what “worthwhile” should mean more broadly (or to others).

Having said all that, I’d like to echo Owen by saying that any practice of hurtful intellectual machismo (which does indeed occur as an organizing force in many areas of mathematics) should be actively fought and changed. However this isn’t a question of which mathematics is or isn’t worthwhile, it is a question of organizing our culture around kindness and inclusivity while fostering a community where we meet each other’s ideas with curiosity, rather than judgement.

(Written on my phone, while waiting for a hurricane to hit, sipping on coffee…. Ciao!)

Owen Lynch

Tue Aug 29 2023

OK, there is an important distinction to have between “worth” and “use” that I wasn’t thinking about!

And perhaps this lies at the heart of my disagreement with Dr. Z. Dr. Z thinks that the short statements with long proofs are worth the most, and I think that the long statements with the short proofs are the most useful. I think that these views are actually somewhat compatible, if we think about the “worth” as something like the “intrinsic reward from discovering the nature of the universe”. And I think that this is certainly worthy!

Then Dr. Z (and many other pure mathematicians) think that we should be doing math for its intrinsic worth, whereas I think that we should put a good amount of that on hold until we make it through the 21st century safely. So in response to “useful for what”, I might say “getting through the 21st century safely.”

And one thing that I didn’t put on my list of things I don’t find useful, but I could have… is string theory. But I think we are in agreement about that. I think “dangerous” is a good way of putting it; dangerous in the same way that high-paying and high-status jobs in making people click on ads or predicting fractional movements in stock prices are dangerous in that it sucks talent away from more pressing matters. But I do believe there’s a eternal, transcendent inevitability about string theory/homotopy theory/etc. that is not present in the stock market or google, that makes it worthwhile in a cosmic sense.

I think that ego is the wrong description of the phenomenon I was trying to put a finger on, though. Even if every individual mathematician has very little ego compared to the average human, they are still heavily influenced by what is seen as valuable by their community. This is an extremely natural, and extremely good human tendency; we want to be valued and respected by our peers. If we didn’t have this, probably society wouldn’t work. Additionally, within the framework of things that are valued, we want to compete for glory. Again, this is an extremely healthy tendency; from competition comes great works. However, the combination of “following community values” and “competition” makes it easy to drift into a relatively isolated community, where the research goals are totally unanchored from even things that the early practitioners of the field would find worthwhile or useful. It seems to me that this happens in all domains of human endeavor, but particularly in academia because it is exceedingly hard to tell the difference between a line of research which will pay off in 40 years, and a line of research which only subsists on self-reference, and if we want to support the former we must put up with the latter.

In response to @Benjamin_Bumpus, I definitely agree that trying to show that other’s math is useless is in itself useless! However, I think that sometimes it is good to “air out” concerns. A lot of mathematics culture is transmitted by graduate students taking on faith from their advisers what sort of things are “worthwhile/useful”. Particularly with things like the twin prime conjecture or the homotopy groups of the spheres, graduate students pick up that if they were to make some new finding that related to these topics, it would be seen as valuable. I want to push back on these “cultural assumptions” and encourage people to think for themselves, develop their own Opinions. Because if you are to guide yourself, you cannot only like things, you also have to dislike things. And that doesn’t mean you should tear down people who do those things; you should maintain a healthy skepticism of your own intuition. But sometimes some open disagreement is good.

Returning to the subject of ego, I think that some amount of ego can help with some of these problems, because while ego can make you vulnerable to the opinions of others, ego can insulate from other’s opinions, giving you the confidence to go out on your own thread.

Anyways, I should probably stop writing about this and do more useful things!

John Carlos Baez

Wed Aug 30 2023

I can’t believe you really believe in your position. First of all, the proof of a statement can never be shorter than the statement itself, since it has to include the statement. So, “long statements with short proofs” has to be defined in some careful way. But there are lots of long statements with relatively short proof that are extremely boring - to me, at least.

Dr. Z’s position does have an inherent kind of logic to it, which reminds me a lot of bitcoin mining and “proof of work”. Having proved a short statement with a very long proof is valuable in that we can then use it as a lemma in other proofs, potentially shortening their proofs a lot. It’s like a form of stored work.

The problem with his position is that it doesn’t distinguish interesting statements from boring ones. In any sufficiently powerful axiom system like Peano arithmetic we know that given any computable function f \colon \mathbb{N} \to \mathbb{N} there are arbitrarily long theorems whose minimum proof length P has P \ge f(L) where L is the theorem statement’s length - at least if the axiom system is consistent. For Dr. Z these would be valuable gems if we take f to be the Ackermann function and L \ge 10000. But by any normal human standard most of these are useless trash.

(Maybe Dr. Z doesn’t work in any fixed axiom system; the way we quickly prove these fake gems exist is by working in a stronger axiom system! I’ve never read him write anything about logic.)

Anyway, my own concepts of “worthwhile” and “useful” are deeply contextual - they depend on what I’m doing, what I should be doing and what I enjoy doing. So I don’t try to reduce them to anything about proof length, and this comment is just for fun.

John Carlos Baez

Wed Aug 30 2023

I would like to push back on this a bit. Most math grad students learn from talking to their peers and mentors to avoid trying to prove the twin prime conjecture or compute homotopy groups of spheres, since these things take a lot of work and the chance of success is low. After Yitang Zhang proved that there are infinitely many pairs of primes of distance \le 70,000,000 from each other, and bunch of people jumped in and reduced that bound to 246. But before he proved this, he worked as an accountant, a delivery worker, at a motel in Kentucky and at a Subway sandwich shop. The lesson is clear: yes we’ll like you if you succeed, but until then… I’ll have a sub with meatballs.

Most math grad students work on projects their advisors recommend, which extend recent progress in an incremental fashion.

Owen Lynch

Wed Aug 30 2023

By this I mean that there are a lot of statements in category theory that require a great deal of throat clearing definitions, but then end up being a trivial proof. Obviously not every long statement with short proof is worthwhile! I was just making a contrast.

Owen Lynch

Wed Aug 30 2023

Hmmm. This is true, but I guess my impression comes from the fact that people will tell me often that their work is on some incremental progress in a big theory, and I’ll ask why the big theory was cooked up, and they will say that it’s related to twin primes or homotopy groups of spheres.

Owen Lynch

Wed Aug 30 2023

I think Bitcoin is a great analogy here. Sometimes it does feel like academic math research is like Bitcoin mining: you get rewarded based on the hardness of the problems you solve, regardless of the why.

Owen Lynch

Wed Aug 30 2023

That is a fun fact though about proof lengths in Peano! I think that perhaps some of those statements would be interesting, or at least the machine for generating such statements would be. It wouldn’t be a terrible heuristic for an automatic mathematician to try and find lemmas with short statements and long proofs and offer them up to humans as possibly helpful.

One of my favorite class of results is results that show that a certain synthetic theory has analytic models. I.e. synthetic differential geometry, or the recent work of the liquid tensor project. This takes all the annoying analytic details and deals with them once and for all, allowing the user to then work freely within the synthetic system. So I definitely get the intuition here.

John Carlos Baez

Wed Aug 30 2023

I guess my impression comes from the fact that people will tell me often that their work is on some incremental progress in a big theory, and I’ll ask why the big theory was cooked up, and they will say that it’s related to twin primes or homotopy groups of spheres.

That sounds like something a mathematician would tell a reporter. Maybe they don’t think you’ll understand what they’re really doing - or maybe they don’t understand the deeper motivations of their line of work. (This often happens with students.)

For example, number theorists talking to reporters often act like Fermat’s Last Theorem is a big deal. It’s easy to explain and it has a romantic story attached to it. But what really matters is the Modularity Theorem! This is much harder to explain but also less silly: it’s a general result connecting elliptic curves to modular forms. Wiles was able to prove Fermat’s Last Theorem just a portion of the Modularity Theorem, but the reason his work is so important is that it paved the way to a full proof of the Modularity Theorem.

I said a bit about why homotopy groups of spheres matter - that is, what deeper issues they are connected to. I don’t understand the twin prime conjecture nearly as well. But the general hope with easy-to-state, hard-to-prove number theory problems is that we can only solve them if we understand more about questions which are much more deeply interesting (because they’re connected to more different subjects).

John Carlos Baez

Thu Aug 31 2023

That is a fun fact though about proof lengths in Peano! I think that perhaps some of those statements would be interesting, or at least the machine for generating such statements would be.

This fact was proved by Gödel. You will be amused and maybe annoyed by his proof:

• John Baez, Insanely long proofs, Azimuth, October 19th, 2012.

Owen Lynch

Thu Aug 31 2023

You see, this kind of thing worries me. I guess I had the experience in undergrad of trusting my professors when I was taking classes that all the stuff I was learning in the classes would end up being super powerful and useful. And sometimes it would, but I eventually learned that the priorities of a typical research mathematician were very different than mine, and I learned to stop taking on faith that I should find interesting what the people I look up to find interesting.

But I had a lot of privilege to have very strong foundations going back to highschool, a lot of exposure to different subjects, and summer research which went in different directions than what I was learning in classes. I’m also quite stubborn. I think if it wasn’t for these traits, I might have ended up doing what my mentors in category theory were doing: i.e. homotopy theory. Because I looked up to them, and they seemed to think it was important. And then three years into graduate school, I would have probably had some sort of existential crisis when I realized that K-theory and spectral sequences weren’t a particularly direct route to better systems theories.

I think it’s essential that students should trust their advisers on what is important to work on. But I also think that advisers have a responsibility to clearly state their motivations on why they find something important, in such a way that a student can evaluate whether their goals are aligned with that line of research before investing the requisite 3 years or however long it takes to actually understand that line of research.

John Carlos Baez

Thu Aug 31 2023

I agree that mentors should talk about why they’re working on what they’re working on - and students should ask them.

When I was an undergrad I spent a lot of time in the math department library browsing books in math and physics, trying to get an overview of different subjects. I was motivated mainly by fundamental physics: quantum field theory, general relativity, quantum gravity, the foundations of quantum mechanics, things like that. So, math that seemed helpful for those topics seemed “useful” to me. (At the time I was not worried about the usefulness of fundamental physics, and I didn’t know that progress in this subject was coming to a halt right around this time and would remain stalled for the rest of my life.) I was also interested in math for its own sake, but I worried a lot about whether it was endless labyrinth where you could spend a lifetime studying any of infinitely many topics. What was the meaning of it all?

By now I’ve spent a lot more time studying pure mathematics and have a much better sense of what I consider important and why I consider it important. I know why homotopy theory is important to me, and it’s not about computing things. But it’s not quick to explain.

Since we live in a world full of unhappiness and problems I feel a strong urge to work on things that will help, like epidemiology and (ultimately, I hope) ways of dealing with climate change and the Anthropocene. But since we live in a world of unhappiness and problems I also need the beauty, clarity and depth of pure mathematics and music to stay happy.

Owen Lynch

Sat Sep 02 2023

One thing people talk about in software library design is “programmer happiness”. I.e., you might have an software library that has a lot of functionality, but is structured in such a way that it’s frustrating to use, it’s not consistent, it doesn’t spark joy.

I think we could evaluate homotopy groups of spheres in a similar light, making deep connections and integrating the world of mathematics sparks joy and wonder in the “mathematical user”, and that in and of itself is a “use”!

Anyways, thanks for engaging with me so much on these issues. One of my goals for localcharts is to develop of a philosophy of why we do what we do, and this has been clarifying for thinking about the range of positions one could take on this.

Eigil Rischel

Tue Sep 26 2023

Every statement that has a proof from the book, is ipso facto, trivial, at least, a posteriori, since all deep statements have long proofs.

This is a bit like saying “it’s easy to factor the products of large primes, at least a posteriori”

Eigil Rischel

Tue Sep 26 2023

Let me elaborate a bit here - there’s a big, massively important difference between things that are trivial “a priori vs a posteriori” - proofs that are easy to find vs proofs that are easy to understand. One might say that, as long as the theorems are easy to understand, it’s not very important whether the proofs are easy to understand, since you can just understand the theorems (and a small set of specialists, or maybe just a computer, can check the proofs).

I don’t think this is really tenable, because to make advances we must expand the set of things that can be understood by humans, possibly aided by tools (to paraphrase Whitehead). In other words, to prove a theorem we must somehow reduce the complexity of the proof into something that we can find, which usually involves finding techniques that simplify existing proofs of moderately difficult theorems into trivialities. (I suppose this is essentially Grothendieck’s “rising sea”)

David Jaz Myers

Thu Sep 28 2023

It might seem rather narrow and pedantic to spend a lot of time calculating specific homotopy groups of spheres, but there is a really easy to understand reason why it’s interesting to study the homotopy groups of spheres in general: They lie at the very bones of logic, and it is completely insane and surprising that there should be anything to study at all.

First, what I mean by “they lie at the very bones of logic” is a very post-HoTT point of view: the homotopy groups of spheres have nothing intrinsically to do with homotopy or spheres, or anything topological or geometric. Rather, we ask the question: suppose we have a type of mathematical object defined by having a single instance with a single nontrivial self-identification. What can we understand about this type? Well, we can see it has many nontrivial self-identifications, since we can compose and invert the one we started with. And with a bit of cleverness, we can show that this exactly characterizes the type: it has a single object (up to identification), and the self identifications of that object form the group of integers.

Ok, to be expected: the integers are the free group on one generator, and we showed that they arise as the group of symmetries of an object which was assumed only to have a non-trivially symmetry. But let’s try another question. Suppose we have a type consisting of a mathematical object so that the reflexive self identification of that object has, itself, a non-trivial self identification. We can show that, as expected, this type has one object up to identification; that this one object has only its reflexive self identification (up to identification); and that this reflexive self-identitfication has the group of integers as its symmetry group of self-identifications (up to identification).

All is right in the world: we put one generator in, we get the group freely generated by a single generator out. But what if we ask the question: does the non-trivial self identification of the trivial self-identification of the object we started with have any non-trivial self-identifications? It turns out that it does! It has integer many of them. And it doesn’t stop there — you actually get non-trivial self-identifications of self-identifications arbitrarily deep. We don’t even know what they all are.

Why!? We put in only one generating self-identification and we get an apparently arbitrary complex algebra of self-identifications. It’s maddening.

Note that this is just the homotopy groups of the sphere, not of the spheres. It only gets worse as you go on (or, better, on a sphere-by-sphere basis, since the homotopy groups eventually have the same pattern to them — a pattern we also don’t fully understand).

On its face this is an affront to intuition: the homotopy groups of the spheres should be the integers at dimension n and nothing else — where could the rest possibly come from!? Turns out they come from all over math, in a sense: the geometry of rotations (O(n)), modular forms and/or elliptic curves, formal group laws in characteristic p, cobordism classes of manifolds, the K-theory of finite sets, and many many more examples.

Kevin Carlson

Fri Oct 06 2023

While we’re on this interesting topic, do you know a good geodesic argument to find the nontrivial self-identification of the nontrivial-self-identification of refl in the type freely generated by a self-identification of refl? I’ve tried a little bit but don’t think I’ve ever figured out a really elementary way to see the nontriviality of the braiding. Even just seeing the generator would be enough I think, if more machinery is needed to actually prove that it’s nontrivial. The Hopf fibration is great but it feels a long way from the bones of logic!

Evan Washington

Fri Oct 06 2023

Hi all! I’m really happy to see a forum where questions like this, which are very close to my heart as a philosopher of mathematics, are being discussed! I have a few points on this, which hopefully aren’t too repetitive and are at least a little conceptually clarifying.

(1) Even if you think mathematics should serve merely as a practical tool for the sciences, you should want mathematicians to pursue the deep/beautiful mathematical truths.

How could this possibly be true? Well, the idea is related to what Wigner toys with in the famous Unreasonable Effectiveness paper. Some parts of mathematics turn out to have practical implications which we did not intend for when we were first puzzling them out:

One example that Owen brought up above was the complex numbers. Historically (iirc), we didn’t know that adding formal solutions to polynomial equations would result in a system adept at describing rotations in space (to use just one example of an unforeseen utility of complex numbers).

I don’t want to belabor the point too much, as I think people above have made more or less identical points, but the idea is just that sometimes we do not discover the practical bits of mathematics without focusing on the conceptual, beauty-guided bits. Of course, very often the arrow of discovery runs the other way and intended applications guide theory. I suppose I’m just trying to say that only focusing on the applications-to-theory direction would be bad for mathematical inquiry at large.

(2) The existence of metamathematics complicates the view of mathematics as a tool for the sciences, but not a science itself.

Mathematics has a very special feature: we can use mathematics to study mathematics! We give that part of mathematics the name, “metamathematics,” or more plainly, logic. As metamathematicians, we might think that we’re merely serving as a tool for mathematics at large. But then it seems like we are viewing mathematics as a science just as much as mathematics views the targets of its applications, like physics or biology, as a science.

This complicates the view because there is in principle no hard division between metamathematics and mathematics. For a familiar example, we view theories in logic as first-class mathematical objects in their own right, say as certain kinds of categories.

So there’s the issue. It seems odd to think that mathematics is a non-science tool for the sciences when we can internalize and use (meta)mathematics as a tool for itself.

I think this point is particularly important here because I view category theory as highly metamathematical in nature. Very often we use category theory to unify and well, categorize, the kinds of mathematics we can do via the kinds of mathematical objects we can study.

(3) The navel-gazing, ego-driven features of mathematics do not exist due to the kinds of mathematics we do or don’t do, but because of structures of academia.

I think that pretty much all professionalized academic subjects fall victim to what detractors might call ego-driven inquiry. My view of this may be quite biased since I’m in a philosophy department and that’s certainly a characterization I’ve heard of my field from others before.

Professional academics exist in a system where being successful is not necessarily paired with being ideal members of an epistemic community, as I’m sure everyone who has experienced academia knows. Very often, we pursue a research question not purely because we think it’s the kind of thing that ought to be studied, but instead because it’s the kind of thing that will be funded, or published, or will lead to higher professional status, et cetera.

What complicates the issue even further is that there is no clean division between research done for the instrumental reasons I just spoke about and research done because we think it’s good or interesting or worthwhile. Most of us split the difference. And most strands of research in the literature are composed of all sorts.

And from the outside, it can be pretty difficult to tell which motivation is which, and pretty easy to think: eh they’re all just making shows of being clever, aren’t they? I’m certainly guilty of that on occasion. It’s always been nice for me, though, to learn to appreciate why researchers care about the questions they do. There’s usually some original good reason, even if it’s become difficult to discern now.

For instance, the study of large cardinals began as a way of seeing just how strong our assumptions need to be to prove theorems much closer to the ground, to everyday mathematics. But from the outside, it’s really easy to imagine set theorists as children just trying to name the largest number they can think of. I really recommend reading some of Pen Maddy’s papers (“Believing the axioms”, part 1 covers ZFC, part 2 covers other axioms like large cardinals). There’s also a little cottage industry churning out finitistic consequences of infinitary principles, like large cardinals, for example in the work of Harvey Friedman.