spekcular

Is the "optimal Julia workflow" written down anywhere?

You may be interested to know that this exact objection has been made in the philosophical literature. See "Causal Fundamentalism in Physics" by Zinkernagel (2010). Available here: https://philsci-archive.pitt.edu/4690/1/CausalFundam.pdf

At the end, the author notes (as you do) that if you consider a finite difference equation with small time steps, there are no pathological solutions. He also mentions that Newton takes this difference equation approach when solving problems in his Principia.

See also "The Norton Dome and the Nineteenth Century Foundations of Determinism" by van Strien:

> Abstract. The recent discovery of an indeterministic system in classical mechanics, the Norton dome, has shown that answering the question whether classical mechanics is deterministic can be a complicated matter. In this paper I show that indeterministic systems similar to the Norton dome were already known in the nineteenth century: I discuss four nineteenth century authors who wrote about such systems, namely Poisson, Duhamel, Boussinesq and Bertrand. However, I argue that their discussion of such systems was very different from the contemporary discussion about the Norton dome, because physicists in the nineteenth century conceived of determinism in essentially different ways: whereas in the contemporary literature on determinism in classical physics, determinism is usually taken to be a property of the equations of physics, in the nineteenth century determinism was primarily taken to be a presupposition of theories in physics, and as such it was not necessarily affected by the possible existence of systems such as the Norton dome.

The author is a professor at Ohio State University, specializing in condensed matter theory. His CV list two works on superconductors and a dissertation on supercapacitors.

There's also a C-R bound for the biased case.

But here the issue is the uncorrected multiple testing and under-reporting of results, not the p-values themselves. Any criterion for judging the presence of an effect is going to suffer from the same issue, if researchers don't pre-register and report all of their analyses (since otherwise you have censored data, "researcher degrees of freedom," and so on). This is really a a problem with the design and reporting of studies, not the analysis method.

AIC is an estimate of prediction error. I would caution against using it for selecting a model for the purpose of inference of e.g. population parameters from some dataset (without producing some additional justification that this is a sensible thing to do). Also, uncertainty quantification after data-dependent model selection can be tricky.

Best practice (as I understand it) is to fix the model ahead of time, before seeing the data, if possible (as in a randomized controlled trial of a new medicine, etc.).

How else do you propose to construct procedures that control type I error and evaluate their properties?

I don't understand. CIs are equivalent to computing a bunch of p-values, by test-interval duality. Should I interpret your points as critiques of simple analyses that only test a single point null of no effect (and go no further)? (I would agree that is bad.)

The items you listed are certainly problems, but p-values don't have much to do with them, as far as I can see. Poor power is an experimental design problem, not a problem with the analysis technique. Not reporting all analyses is a data censoring problem (this is what I understand "specification curve analysis" to mean, based on some Googling - let me know if I misinterpreted). Again, this can't really be fixed at the analysis stage (at least without strong assumptions on the form of the censoring). The replication crisis is a combination of these these two things, and other design issues.

I think if hypothesis testing is understood properly, these objections don't have much teeth.

1. Typically we use p-values to construct confidence intervals, answering the concern about quantifying the effect size. (That is, the confidence interval is the collection of all values not rejected by the hypothesis test.)

2. P-values control type I error. Well-powered designs control type I and type II error. Good control of these errors is a kind of minimal requirement for a statistical procedure. Your example shows that we should perhaps consider more than just these aspects, but we should certainly be suspicious of any procedure that doesn't have good type I and II error control.

3. This is a problem with any kind of statistical modeling, and is not specific to p-values. All statistical techniques make assumptions that generally render them invalid when violated.

Is there a modern reference you would recommend?

My argument is that key claims of the paper are factually incorrect. For example, there was no "confession" by Karplus and Kroll. (At least, none is cited as far as I see - please let me know if I am missing something.)

If a mathematical technique helps understand and predict nature, why not use it? The quote criticizing the method misunderstands it. It's certainly not "wrong" or "absurd."

I dislike the paper because it is sensationalist and highly misleading. For example, as far as I can tell, Karplus and Kroll didn't "confess" to anything (no direct quote is provided in the paper); we just have a secondhand assertion by Feynman. Nothing they did is "fraud," as the author claims - this is false and defamatory. Further, the issue got wrapped up by Petermann in 1957; the author is just annoyed that he didn't publish full details of the calculations. The suggestion that there is somehow lingering uncertainty is just wrong.

I no particular wishes for the author, other than that he cease writing bad papers.

This has already been posted a few times: https://news.ycombinator.com/item?id=31431033

The summary is that the author doesn't know what he's talking about.

I see - I understood "liberal arts program" above to mean a liberal arts college in general (typically offering a mathematics major). I agree that this reading list is better suited for something like "history of math for humanities students."

Yes, it is substantially different with respect to content than standard undergraduate mathematics programs. It covers a few historically important texts and does not teach (if those texts are any indication) most of what is usually taught in an undergraduate math degree. (A poster above writes: "Freshman math was almost entirely the study of Euclid and Nicomachus.")

I believe the person you're replying to understands that. The claim is that this approach is really bad way to learn math.

As someone who has learned and taught a lot of math, I agree with that claim.

The experiment is part of a larger research program to study delayed gratification. It was never intended to help parents raise their children. Asking for immediate applications is an odd standard for basic science research. (Unless you reject the value of basic science research entirely.)

Further, the result in a recent replication [1] was a correlation of .28 between the time to ring the bell (to get the marshmallow) and academic achievement. That's not exactly the trivial "4% less likely" effect in your caricature.

(You may also wish to double check your spelling of "marshmallow.")

[1] https://www.jasoncollins.blog/posts/the-marshmallow-test-hel...

The marshmallow effect replicated (IIRC), and is probably correct, unlike the power posing stuff. That behavior in a single trial in childhood moderately predicts success in adulthood seems like an interesting fact about humans.

What's accepted by mathematicians as the foundation of mathematics is an objective fact about the mathematical community. You can look up the answer to the question "What is the standard, commonly accepted foundation for mathematics?" in any number of reference books. Some options to get you started: Kunen's Foundations of Mathematics; Jech's Set Theory (super common books for graduate students).

My challenge to you: find a single book written in the last, say 50 years, where the answer to this question is not ZFC (or ZF with some equivocation about whether we should accept choice).

Re: "Equivalence is equivalent to equality," first of all, most mathematicians would take this to be false. Like, if "x" stands for cartesian product, they would say (A x B) x C and A x (B x C) are different objects. (This is a point commonly made in undergraduate algebra classes, and the reason they would say this is of course they they implicitly think of everything as sets, since set theory is the standard foundation!) They are isomorphic objects, but not equal ones. Second, to the extent that mathematicians suppress isomorphisms like this in their writing, this is not a new observation. We've known that mathematicians do this for decades, and in principle we could always unravel such isomorphisms when writing things down carefully if we needed to. This is not some special insight of HoTT. Compare to the forcing example I gave - this is a genuinely new insight about the Calkin algebra facilitated by "classical" methods of mathematical logic.

Re: DNNs, the question of what is a semantics for DNN does not count as an example, no. What would count: statements about things like consistency, independence, shapes, numbers, etc. It's cool that you can use HoTT for engineering things but it's not an application to discovering new pure mathematics or the consistency/proof strength/independence/etc. of that mathematics. The latter is the usual definition of "metamathematics."

Here's an example of a (true) metamathematical statement: HoTT is consistent if ZFC plus two inaccessible cardinals is consistent. (Interestingly, this is the best argument I'm aware of for the claim that HoTT is consistent, and its power derives largely from the fact that ZFC is the Gold Standard for foundations.)

Facilitating metamathematical inquiry of this kind is perhaps the primary reason mathematicians are still interested in set theory and classical logic. (I include here large cardinals, model theory, etc. For further discussion, see the books I mentioned above.)

I don't think the principles that HoTT wants to take as axiomatic are actually fundamental or ontologically basic enough to be made axiomatic. Is that so shocking?

We've been over this. To say "It's an objective fact that the professional mathematical community has decided that ZFC is the standard foundations" is not inconsistent with your claim that "there a portions of mathematics never formalized on ZFC." Both claims are true!

Also, re: the mathematical point, I asked above: "What new metamathematical statements - recognizable to an ordinary mathematician with no particular interest in topos theory or HoTT - has this led to?" You proceeded to give examples that did not fit this description. If you agree that HoTT is not good for metamathematical inquiry, then great, we agree on something!

Also, DNNs are (definitionally) not a topic in pure mathematics.

With respect, I find your point of view "oddly narrow-minded," and not representative of what most mathematicians think about these issues. Taking these points in order:

1) I haven't written anything about constructive logic because I don't care for it, and other issues seemed more interesting to discuss. Further, the law of excluded middle has a robust presence in modern mathematical practice. A foundational system without LEM essentially by definition cannot replace ZFC for the purpose that ZFC is used for within modern mathematics. I understood the discussion to be about what should be used to ground mathematical practice.

2) "You have opinions about what you'd like from foundations." Not really. Rather, there are different goals one might want a foundational system to achieve, and we can discuss the merits of systems based on how well they meet our desired goals. I have already said, for example, that if your goal is the practical formalization of complex proofs, then type theory might very well be suitable for achieving that goal (as demonstrated by Lean).

My objections in this thread have always been that HoTT proponents are not always precise about what goals they want to achieve, and why they think HoTT is best for achieving them. That is true even if I don't care for the stated goals.

3) "They are dogmatic and are not the opinions of those mathematicians working on foundations. Those mathematicians are interested in constructive logic, computability, the computational meaning of mathematics, replacing sets with topological spaces, replacing sets with objects closer to mathematical practice, etc." The work you've just characterized is not mainstream within the community of mathematicians working on foundations and logic. Go look at what gets published in the Journal of Mathematical Logic, for example. It's just a sociological fact that the constructivist stuff (in particular) is somewhat niche (outside of say reverse mathematics, which is different than what you noted). The views I express are fairly widespread, though I put them a bit more sharply than others.

Here's a question to illustrate this point: Who at an R1 math department works primarily on the issues you mentioned? Who got hired or got tenure on the basis of this work? I can't think of anyone off the top of my head. There are at best a few topologists who got hired for their topological work who branched out into these things later. I don't doubt that if you search you can find a handful of examples - but that number is going to be much smaller than the equivalent number of people doing "classical" set theory and logic.

4) What's so wrong with not wanting the univalence axiom in my foundational system? Or thinking that this axiom is in fact a negative? It's not very ontologically primitive, after all.

The disagreement is about whether there are reasons aside from facilitating formalization to care about HoTT. (Because if not, it seems like we should all be jumping on the Lean bandwagon instead.)

It's an objective fact that the professional mathematical community has decided that ZFC is the standard foundations. The point of my post was not to explain my experience with textbooks, it was to note that you can check virtually any published source on this topic to find a reference for that claim.

Extracting semantic content of DNNs is not a pure mathematical or metamathematical problem; it is an applied problem. Again, I'll happily admit type theory can be good for engineering stuff. But you claimed it was good for metamathematical inquiry. I'm looking for a statement about things like consistency, independence, shapes, numbers, etc. Set theoretical inquiry gave us tons of those, as I pointed out above.

I understand your last sentence to agree with the statement that everything could be formalized in ZFC given sufficient effort. (I do not really care by what means we know this can be done.) If so, then I'm not sure why you disagree with what I wrote previously.

Come on now. I just told in what sense ZFC has not been replaced, and you mentioned something different. No one ever claimed people actually wrote down their proofs in ZFC - again, that was never the purpose.

Are there any which don’t exclusively apply to the mechanics of set theory itself?

Forcing has been applied to a variety of statements, including those about "normal" mathematics. The first example that comes to mind is the question of whether all automorphisms of the Calkin algebra are inner (Farah, 2011). There are many, many others.

That the equivalence of algebra/geometry commutes with the equivalence of proof/computation has two practical effects:

You have still not given a statement an ordinary mathematician should be interested in! Type theory might good for engineering things - I'm totally on board with that. But if you claim HoTT has meta-mathematical interest, you need to give a meta-mathematical justification. That is, you need to prove something new (and interesting).

Tackling the second part first: Yes, mathematicians use all sorts of reasoning in pursuit of mathematical truth. Sometimes this reasoning is mildly sloppy, or abuses notation. So what? We all know in principle that this reasoning can be written down formally in ZFC with enough effort, if we really needed to, and this is enough to satisfy us. If you go to a mathematician and claim their work in number theory isn't actually rigorous because they wrote "7" to mean the equivalence class of 7 mod p, instead of a separate symbol like a 7 with an overbar, they will laugh at you.

But the whole point is how to keep track of what questions one is evidently allowed to ask - what questions are demonstrably not as ill-posed as "is the number 7 equal to the trivial group".

I don't understand what you mean by "questions one is evidently allowed to ask." You can ask any questions you want. In particular, as long as we agree that whatever question you want to ask can be translated into a question about sets, we can resolve that question by answering the analogous question in the framework of ZFC. All I object to is the claim that some set is, ontologically speaking, the same as the number 7, and hence that set theory proves "junk theorems."

Here's a silly analogy. Suppose we work at NASA and we want to fly a rocket to the moon. We agree that the answer the question of how much fuel we need, we can write a computer simulation with a representation of the rocket, the earth, the moon, and so on. We run the simulation and answer our question in that simulation, and if the simulation is a good representation of reality that also answers our question in reality, and then we go to the moon and everyone is happy. However, nowhere in this process do we believe that the rocket in the simulation is the same thing as the rocket IRL.

What does it mean for "a thing to be the actual thing"? I don't think any formalization you can write down will "actually" be the number 7 (though I'm happy to consider any attempt to do this with an open mind).

You're very dogmatic about what people should accept from a foundation. You seem happy to accept an approach that has very little to say about practice, which is certainly an opinion, but not universally held.

There is a point of view that foundations should reflect and inform practice - or maybe even challenge practice - and are not just there to make you feel more comfortable philosophically.

I don't understand this comment. Studying set theory has said a lot about mathematical practice - for instance, about what we can and can't hope to prove in certain systems, or about what axioms are needed for what statements. That's important stuff!

More generally, there's the question of what you hope to accomplish by supplying a foundation for mathematics. Any value claim about some foundational system is contingent on what goal you have. As I said above, if that goal is actually writing down computer-checkable formalized versions of complex proofs, then ZFC is perhaps not the foundation you want to use.

But, historically speaking, that was not what people had in mind. There was a desire to reduce mathematical reasoning to a few philosophically basic concepts so that we could be confident in its coherence and consistency. And a desire for providing a framework for studying mathematical reasoning itself. I think it's really important to understand this historical context, otherwise you end up with misleading claims like "ZFC is a bad foundational system because it doesn't help me formalize my research papers."

Further, the reason I get grumpy when HoTT stuff is posted here is that the postings are rarely explicit about just why, exactly, they think HoTT should supplant ZFC as the accepted foundation of mathematics (or even exist on equal footing, creating a plurality of foundational systems). If you take the goal of a foundational system to be practically formalizing proofs, we have no evidence HoTT is particularly suited for this, and (as far as I know) no serious movement by the HoTT community to actually realize this vision (relative to what the Lean community is doing). I'm not claiming the first mover in some space should always dominate, just that if the HoTT people want to arguing for their foundational system on the grounds that it assists in formalizing math, maybe they should actually demonstrate their superiority by formalizing some math. For a longer comment on this, see: https://xenaproject.wordpress.com/2020/02/09/where-is-the-fa....

So if we disregard formalization, the arguments in favor of HoTT that remain are philosophical ones. But, as I've explained elsewhere in this thread, I find them all misguided. They all basically seem like arguments about aesthetics but don't actually tell me why HoTT is better than ZFC for the philosophical goals mentioned above.

I came to a different conclusion: they very much meant to ground mathematics in ZFC formalisms — and went to the effort of projects like Principia trying to achieve that. ZFC was a failure in this regard, almost immediately replaced by category theory and type theory.

ZFC hasn't been "replaced" by anything. The standard line in all published textbooks that I'm aware of is that ZFC is the accepted (by the professional mathematical community) foundation for doing mathematics (assuming this question is even raised). Even the type theorists admit this!

That’s why we replaced Turing machines with type theories, lambda calculus, automata, etc. Our modern research uses these formalisms because they’re outright better.

The Turing machine is a fundamental concept in theoretical CS that isn't going anywhere. Consider that the standard textbook on the theory of computation (Sipser's) has three parts, and the second is entirely devoted to studying computability using the Turing machine concept. Or that the strength of pushdown automata is usually explained in relation to Turing machines.

OK, so what are the concrete fruits of this?

The first two things you listed are not metamathematical statements. I'm not sure what you mean by the third. (Sure, many things can be recognized as special cases of category-specific concepts. But that's a claim about category theory, not HoTT.)

This is also a weird demand while leading off with how people don’t actually work in ZFC.

People do not write their papers in first order logic starting from the ZFC axioms, that's true. But the study of set theory has led to large number of metamathematical successes, such as forcing and the independence of the continuum hypothesis.

Nevertheless, topos theory is what explains the algebra-geometry duality: you have two languages (type theories) that map to isomorphic categories. You can then extend that idea to things like the Curry-Howard square.

OK, so what's the actual concrete statement an ordinary mathematician should be interested in?