spekcular

I think this is a common misconception. In set theory, one does not say that some set is the same as (ontologically) the number 7. After all, we understood what the number 7 is far before we had the concept of an abstract set in our mathematical vocabulary.

Rather, set theory lets us say that questions about 7 are equivalent to other questions about sets. So, 7 is prime if and only if some claim about sets holds, stuff like that. We do indeed usually pick some particular set to represent the number 7 for the purpose of this translation, but that isn't a claim that 7 is that set (since, e.g., there are many ways to choose a set to represent 7). So one cannot ask questions like 'is the number 7 equal to the trivial group?' within ZFC but only questions like 'is the set I've chosen to represent 7 equal to the set I've chosen to represent the trivial group,' which - while strange - shouldn't cause any philosophical worries.

I suppose to some extent this is a matter of taste. I'll just say that, in my experience, people are typically very comfortable with, e.g., logical connectives and the primitive notion of a set of objects from grade school mathematics education. So this framework is "natural" and readily believed.

Further, in ZFC, the only basic notation is that of a set. In something like the calculus of constructions, there are five fundamental notions (if I remember correctly). From the standpoint of ontological parsimony, that's a win for ZFC.

Axiom of separation just says we can make subsets of things - I think this is not so hard to swallow. I'm curious what you find counterintuitive about it.

Yes, it's not so clear to me either. But I'm willing to grant this point for the sake of the argument.

The point of the ZFC axioms was never to write down actual formalizations of complicated proofs. It was to provide a small, parsimonious foundation for all of mathematics with a minimal number of "obvious" commitments, to give us confidence that the mathematics we're doing is consistent, and to provide a basis for metamathematical investigations. (Roughly speaking - this compresses a lot of history. Also ZFC may not be the optimal set theory for doing this, and its choice as the standard foundation is somewhat historically contingent.)

A good analogy is the idea of a Turing machine in theoretical CS. It's an idealized model for studying the theory of computation. To object that it's impractical to write a complicated program like a computer algebra system using the Turning machine formalism misses the point.

> The key idea of univalence is an axiom that says equivalence is equivalent to equality; and that if we only want equivalence as our standard, that we can substitute proofs of equivalence for proofs of equality.

I just said I don't want equivalence to be equivalent to equality!

> The main insight is that topology of diagrams determines the semantics of your logic; which helps us explore concepts like abstraction and proof simplification. (This relates to topos theory — which creeps up in CS fairly often.)

OK, so what are the concrete fruits of this? What new metamathematical statements - recognizable to an ordinary mathematician with no particular interest in topos theory or HoTT - has this led to?

I realize it's Christmas Eve, but this post tempts my inner curmudgeon.

I do not understand why homotopy type theory posts are so popular on this website. My view is that all the "philosophical" arguments in favor of it (vs. the standard set theory foundations) misunderstand the issues at play. Further, the "practical" arguments in terms of facilitating formalization are not so compelling given the HoTT people haven't actually (as far as I know) formalized much mathematics - whereas (seemingly) less ideological communities like users of Lean have made great progress.

To expand on the comment about the philosophical arguments: take for example the abstract of this article. It states:

> It is common in mathematical practice to consider equivalent objects to be the same, for example, to identify isomorphic groups. In set theory it is not possible to make this common practice formal. For example, there are as many distinct trivial groups in set theory as there are distinct singleton sets. Type theory, on the other hand, takes a more structural approach to the foundations of mathematics that accommodates the univalence axiom. This, however, requires us to rethink what it means for two objects to be equal.

It is sometimes quite useful in practice to recognize that two isomorphic objects are not literally the same. So I am skeptical of any approach that wants to blur those distinctions.

Also, more to the point: ZFC does everything we need a foundation to do extremely well, except serve as a basis for practical formalization of proofs.

People have posted books on arxiv for at least a decade. Their rules state: "Submissions to arXiv should be topical and refereeable scientific contributions that follow accepted standards of scholarly communication."

Hi Dang,

There's no personal attack here. I'm sorry if that comment comes across as curt, but the post I responded is (in my opinion) grossly misleading and deserves pushback. For example, consider the statement: "If the proof has a flaw, the issue will be technical and difficult to uncover," made by someone claiming years of experience as a math professor thinking about this question. This is easily identifiable as wrong, because the purported proof is just 7 pages (actually less than that due to extraneous material) and does not use any particularly technical mathematics (a strong undergraduate major probably knows enough to comprehend what's going on). Indeed, people found the error in (less than) 12 hours after that comment was made.

The comment about senility is not a "swipe." It is a very real problem in the mathematics community. Mathematicians get old and are sometimes afflicted by dementia, and this unfortunately can manifest as hopeless attempts at famous problems. Atiyah's "proof" of the Riemann Hypothesis right before his death is perhaps the most well known example, but there are others that (thankfully) aren't disseminated publicly. In the pre-internet age, journal editors were able to make such things quietly disappear. But now we have the arxiv. This is valuable context for understanding why two mathematicians with distinguished publication histories might be posting an incorrect proof, which had not been provided by other comments.

That being said, I will endeavor to phrase such comments more carefully in the future. Thank you for your message.

It's not bizarre at all. The math community has unfortunately been down this road many times before. When an 80-year-old announces a 7 page proof of a famous problem, the smart money is on the proof being wrong. As the comments elsewhere on this story indicate, this heuristic turned out to be correct. The only new twist is that we have two 80-year-olds this time, not one.

To be clear, I don't like this state of affairs. As suggested above, the best course of action seems to be to ignore the posting.

You're not missing anything.

I don't think asymptotic estimates of that form suffice to treat this problem. (Where else in combinatorics has an argument of this form succeeded? What intuitive reason is there to expect it to succeed here?)

Specifically I think section 4 is basically nonsense. (I see Sniffnoy has already pointed this out below.)

(Re: your comment, Theorem 7 is going to fail below the smallest counterexample, right? This is bad, imprecise writing - a red flag.)

See above clarification about the bad writing.

Yes. How does it bear on what I wrote?

Yeah, my guess is that both are senile if they're putting this on the arxiv.

Second-order evidence: Old mathematicians (~80). Famous problem. Weird, imprecise writing style. No mention of the proof by mainstream mathematical news sources (breakthroughs are usually accompanied by excited blogging/tweeting). No acknowledgements directed at other mathematicians who have checked or commented on the proof.

[deleted argument here; replaced by more precise comment below]

My tone is harsh because I think the best thing to do is to quietly ignore it, similar to how the community treated Atiyah's claims of a RH proof at the end of his life.

Your post feels like a dispatch from bizarro-world.

There is a good amount of second-order evidence that the proof is wrong. Further, I skimmed the introduction, and it seems the indicated approach cannot possibly work. My guess is that both authors are senile. (They're quite old.)

If you give me decent odds, I'd be happy to bet against you regarding the proof's correctness. Would you take 1:1?

Thanks! I'd be interested in what you have to say, if you get a chance to read in detail.

The blog post talks about inference, not prediction, so I find it odd you keep bringing up prediction tasks. There are interesting questions and differences here, but it is very much not the subject of the post.

A standard frequentist tool for making predictions is the prediction interval. This is the appropriate comparison point for Bayesian prediction methods, and exactly the same issues arise as in the comparison of confidence intervals to credible intervals (or posteriors). Namely, frequentist prediction intervals have guaranteed error control, while Bayesian predictions generally do not. So in certain cases you have to choose between being right most of time about your predictions, and being Bayesian.

Well, I am not really interested in cookie jars. But I am interested in, for example, particle physics. There we need need simple ways to communicate point estimates and the associated uncertainties for various parameters of nature. Intervals are a convenient way to do this. Frequentist confidence intervals have the virtue that they will cover the true parameter at the nominal rate. Bayesian credible intervals in general have no such guarantee. In many cases we can find Bayesian-inspired interval estimators that have good coverage properties. But in some cases there is an irreconcilable conflict. And there you have to choose between long-run correctness and being Bayesian.

You might claim that we should do away with intervals and just report posteriors for all physical quantities. This complicates matters slightly without solving the problem. If the true parameters, when ultimately known, consistently end up in very low density regions of the probability distribution (such as far in the tails), we would regard our uncertainty estimates as poor. Again, it is not hard to construct examples where Bayesian methods have poor coverage properties in this sense.

(Also, a minor point: Regarding "Do you need to select a strategy up front which gives at least a 70% chance of being right about the jar over iterations where the jar is fixed but the data varies?", one does not need to fix the jar for frequentist methods to have good guarantees. See Wasserman's simulation with the median.)

Re: "Given that I drew a cookie with 2 chips on the first draw, what is the chance I draw a cookie with 0 chips on my second draw?", this is not a question about estimating an unknown parameter of a distribution, so it's not statistical in the sense Wasserman is talking about. It's just an elementary probability question that requires knowing something about the jars to answer. Both frequentist and Bayesian statisticians agree on the validity of Bayes rule (and hence how to answer this question once the relevant information is known or assumed); where they differ is on how to conceptualize and estimate unknown parameters of probability distributions.

Honestly, I think Wasserman does a better job. The cookie interval example gets the fact that frequentists require uniform coverage properties with respect to the unknown parameter right. But the "when you pull a cookie with 3 chips your interval is only correct 41% of the time" thing isn't really an essential Bayesian vs. Frequentist issue. As Wasserman notes, coverage is a minimal requirement for something being a confidence interval; we usually also construct them to avoid obvious deficiencies. All this objection shows is that the particular procedure in the example might not be the best one; it's not an argument that can be applied to all CIs in general. (And it's clear, if you play with the numbers, that the example can be improved.)

Also, regarding "But note that we probably don't really care about the confidence interval or credibility interval." Many times we do - giving a point estimate and an associated quantification of its uncertainty is one of the most basic statistical tasks.

Further, it's somewhat misleading to critique frequentists by saying they don't give probabilities for P(Jar | Chips), because in the frequentist setup the jar is a fixed and unknown parameter, not stochastic. For the two-cookie setting, it's trivial to generalize the construction in the M.SE post, so saying "frquentists can't track evidence to get better predictions" is simply wrong.

Did you read Wasserman's article? There's a difference between a frequentist/Bayesian interpretation of probability and a frequentist/Bayesian method of inference. I don't have to take a position on what probability "really means" to use either kind of inference method. (As the article says, the true difference has a lot more to do with wanting guaranteed coverage...)

Other great tracks:

Prelude in G minor, Op. 23, No. 5.

Piano Concerto 2. It's long but at least listen to the first 30 seconds, up until the point when the orchestra comes in. This is (in my opinion) one of the greatest moments in all of Western art music.

I don't think Nick Polson is a bad or stupid person. I never said this. In fact, as I said above, I believe he is quite mathematically competent. But even competent people make mistakes.

Norms of scholarly communication are not a personal opinion.

You have also curiously avoided my question about whether it is improper to knowingly disseminate incorrect results.

Arxiv's submission policy says: "Submissions to arXiv should be topical and refereeable scientific contributions that follow accepted standards of scholarly communication." (https://arxiv.org/help/submit)

It against the prevailing norms of scholarly communication to publish results with serious errors known to the author.

I agree YouTube does not have this policy. I still find incorrectly claiming a proof of RH on YouTube distasteful, for similar reasons.

I personally know a mathematician who has pointed out the mistakes to him. But also, Polson good enough at math himself that he should be aware of these points. I would criticize him just the same if he knowingly published false economics results.

I believe knowingly disseminating incorrect results is wrong. This is a violation of fundamental academic standards; we would not tolerate it in any other scientific field. Do you disagree?

He has continued to update the paper (as recently as last year), it has not been retracted, and he appears to maintain the proof is correct on his YouTube channel.

We all make mistakes, and no one would really care if he admitted this. What makes the case notable is that he has enough mathematical training that he should be able recognize the proof is wrong. Especially after the errors are uncovered by others and communicated to him. Continuing to assert the proof is correct after errors have been found is bizarre.

The standard being applied here is just that the work is correct. Polson's paper on RH is wrong.

It is bad practice to post incorrect results and not retract them when this is pointed out.

It's worth noting that one of the authors of the cited paper [1] (Nick Polson) is infamous for claiming (incorrectly) a proof of the Riemann hypothesis [2].

This case is somewhat strange because he's not the usual mathematical crank; he's actually a quite well-recognized economics researcher who is clearly mathematically competent. But for some reason he persists. (If you search his name, you can find his YouTube channel where he lectures on his RH work...)

[1] https://arxiv.org/abs/2208.09563

[2] https://arxiv.org/abs/1708.02653.

The Four Seasons is not homophonic music? It varies by season but IIRC there's definitely some homophonic writing in there.

People like Vivaldi writing homophonic music.

I think this is common knowledge and can be found in a lot of music history books. He was essentially the culmination of a contrapuntal tradition, after which people started writing more homophonic music.

Some supporting evidence might be:

1) He was basically forgotten after his death until being rediscovered by Mendelssohn (https://www.loc.gov/item/ihas.200156436/). Googling this "fact," I also found this somewhat dissenting post: https://notanothermusichistorycliche.blogspot.com/2016/06/ho....

2) I recall remarks from his sons somewhere about their father being old-fashioned, though I can't find them right now.

Re: GEB, I can't speak to hofstadter's psychology, sorry.

I agree with the claim that problem solving is essential to learning mathematics. And I have had the exact same experience where I did well on math exams by ignoring most of the theory and proofs of main results, and focusing solely on examples and problem solving.

However, I think straight-up memorizing definitions and theorem statements is really useful for problem-solving/exam prep, just so they're at your fingertips. There's no way you're passing a real analysis exam if you can't regurgitate the epsilon-delta definition of a limit in your sleep.

What seems to occur (at least for me) is that you naturally memorize all of these things in a somewhat inefficient fashion by doing problems. If the concept gets used in enough problems, it slowly burrows its way into your memory - and this is a very durable kind of memory, as you point out. But I do think for things like graduate school qualifying exams you can "juice" the process by explicitly memorizing core material.

Probably it's not as useful for doing research, though.