ocfnash

Mathematicians are interested in which natural numbers k can be expressed as a sum of three cubes. Prior to this year, it had been established that this is possible for all k < 1000 except for the following thirteen values:

33, 42, 114, 165, 390, 579, 627, 633, 732, 795, 906, 921, 975.

Earlier this year a solution for k=33 was found [1], so 42 was the next unknown value.

[1] Brooker, A., "CRACKING THE PROBLEM WITH 33", https://people.maths.bris.ac.uk/~maarb/papers/cubesv1.pdf

Well they claim it is a HoTT (thus presumably univalent) and furthermore has higher inductive types, neither of which exist in Coq's CIC.

For example, they emphasise that function extensionality is a theorem here: https://arend-lang.github.io/about/arend-features (not true in CIC).

It would just be nice to see a list of the rules.

Still I don't want to get hung up on this; the rules must exist somewhere and presumably will become more discoverable. The project looks superb.

Wow, I am delighted to see this!

However I cannot find a precise reference for the chosen type theory.

E.g., is univalence a theorem in their type theory? I presume it is given that they say their language has "syntax similar to cubical type theory" but I could not say for sure.

What I'm looking for is a reference containing the actual typing rules, like this one for Coq: https://coq.inria.fr/refman/language/cic.html#typing-rules

rather than the syntax of the language used for building these terms.

If you can remember enough of it you might try writing down a Parsons Code and searching against, say: https://www.musipedia.org/melodic_contour.html

https://en.wikipedia.org/wiki/Parsons_code

Right; indeed they have _definitionally_ at most one inhabitant. Swiping the following spec from the page you link:

  Definition irrelevance (A:SProp) (P:A -> Prop) (x:A) (v:P x) (y:A) : P y := v.

the point is that `irrelevance` consumes an inhabitant `v` of the Prop `P x` and is supposed to "return" an inhabitant of the Prop `P y`. A priori `P x` and `P y` are different types but since `x` and `y` are both inhabitants of a type whose sort is `SProp`, they are definitionally equal and so `v` is definitionally a valid inhabitant of `P y`. This justifies the implementation of `irrelevance` as `v`.

I can imagine some other illustrative examples but I think I'll wait till I've played with SProp to confirm I'm not barking up the wrong end of the stick.

As well as a new sort, SProp!

https://coq.github.io/doc/v8.10/refman/changes.html#version-...

I'm Irish; many of us are ashamed of how we treat our bogs. We have tiny peat-burning power stations which:

  * Are extremely polluting
  * Destroy a unique ecosystem
  * Are loss-making

all for the sake of "protecting" a few local jobs.

A wonderful account of this is given in Ellenberg's "How Not to Be Wrong": https://en.wikipedia.org/wiki/How_Not_to_Be_Wrong

I highly recommend the book; it is a popular mathematics book, written by a real mathematician, discussing some real mathematics, with an engaging style.

Your remarks bring me close to the border of my limited knowledge of model theory so I must be careful with my response.

I believe the answer to your question:

> Do other considered set theories offer any improvements over ZFC in these specific respects?

is "no", and that you essentially answer this yourself with the following paraphrasing of Löwenheim–Skolem:

> As long as you stay within first-order predicate logic, a theory of sets will run into such issues.

So if we opt Lawvere set theory I think we just do the same thing as if we had opted for ZCF, i.e., just assume we have a model (perhaps provided by some higher order logical system).

However in my opinion, we do have a theory with a much more intuitive set of axioms.

I am a geometer by training.

I'm not at all qualified to answer such a broad question but I'll share my amateur opinions for what they're worth.

I believe people are gradually coming round to the point of view that constructive mathematics (including intuitionism) is a useful generalization of classical mathematics, rather than a handicap.

Proof assistants, while still fairly niche, continue to get more attention and the fact that constructive mathematics tends to give "proofs that compute" helps.

For what it's worth, I waffled on about this a little a few months ago right here: https://news.ycombinator.com/item?id=18404914

In my opinion HoTT is the most interesting subject in this area but we have yet to figure out exactly what its role is, and the extent to which it should serve in foundations. However the fact that it is a deep theory with significant value independent of its foundational role must surely help the constructive point of view. I think it's fair to say "Book HoTT" is not fully constructive since univalence is an axiom but this seems to have been resolved with the introduction of cubical type theory.

I also suspect the majority of mathematicians still spend very little time thinking about foundations.

A substantial portion of this text appears to be concerned with traditional Zermelo–Fraenkel set theory (and its extensions).

I have gradually come to believe that ZF theory has received a disproportionate amount of attention on account of the fact that it serves as the "official" foundations of mathematics, but that it is not an especially beautiful, or useful, structure.

I believe that ZF theory is an interesting object, worthy of mathematical study, but _not_ the best candidate for the foundations of mathematics! I am very happy to see that this year's Chauvenet Prize [1] was won by Tom Leinster's "Rethinking set theory", in which he highlights that Lawvere set theory looks like a much better candidate. I cannot do better than recommend you look at Leinster's superb article.

[1] MAA, Chauvenet Prize, https://www.maa.org/programs-and-communities/member-communit...

[2] Leinster, T., "Rethinking set theory", https://arxiv.org/abs/1212.6543

It continues forever! See here for example: https://mathoverflow.net/questions/215187/is-there-a-referen...

I believe you are just running into the limits of double precision arithmetic; indeed log_2((10^8)^2) > 53.

Here's a fun fact about the Mandelbrot set, which I will communicate in Python in the hope that you can have a little fun witnessing the results:

  def N(eps):
    c = -0.75 + eps*1j
    n = 0
    z = 0
    while abs(z) < 2:
      z = z*z + c
      n += 1
    return n

  [N(eps) for eps in [0.1, 0.01, 0.001, 0.0001, 0.00001, 0.000001]]

>> It turns out that the Komodo sex determination system means the offspring are always male.

> Do you mean when it is _not_ parthenogenenis? How does this work?

I mean all Komodo offspring produced by parthenogenenis are male even though offspring from usual sexual reproduction in Komodos can be either gender. The reason is that the Komodo sex determination system is logically opposite to that of mammals. Specifically, whereas in mammals, a pair of homologous sex chromosomes XX, produces a female, in Komodos this produces a male, ZZ. (Parthenogenenis means there is also the possibility of Komodo WW embryo but these are not viable.)

Happy to hear someone else thinks this is interesting.

Just recently I learned that Komodo dragons have the unusual feature of being able to reproduce via parthenogenesis. This means that a female dragon, can become pregnant spontaneously!

Apparently the cell which grows into the baby dragon is formed from an ordinary egg cell that duplicates each of its chromosomes rather than having a second set of chromosomes provided by a male sperm cell, as in sexual reproduction. It turns out that the Komodo sex determination system means the offspring are always male.

I believe this means that the offspring are thus completely homozygous, though not clones of their mother because the egg chromosomes were formed by the usual meiosis. Even more amazing (I think) is that there are apparently some boa snakes which can also reproduce via parthenogenesis but whose sex determination system makes all offspring female. IIUC, if any of these daughters were also to reproduce via parthenogenesis, then their offspring would indeed be clones of their mothers. A sort of genetic end point.

I have a Chrome bookmarklet specially for Bloomberg. Instant relief with a single click:

javascript: document.getElementById('paywall-banner').remove(), document.getElementsByClassName('right-rail')[0].remove(), document.getElementsByClassName('left-column')[0].remove(), document.getElementById('navi').remove(), document.getElementsByClassName('zipr-recirc')[0].remove()

Actually I think we're in agreement here: I didn't make it clear but the nominal figure to which I was referring was the magnitude claimed free. By saying "extra free" they get to write down 10% instead of 9%.

I also agree the difference is small in this case but I'd argue:

  * Small wins are still wins.

  * The difference is not so small with bigger percentages.

Imagine I decide to tweak my margins for a time and sell 1.5Kg of cereal for the price I previously sold 1Kg. I could say "33% free" (relative to old price) or "50% extra free".

I quite enjoy mentally parsing these "offers" in logically equivalent ways. E.g., "buy one get one free" as "only sold in units of two" or even "each purchase of one requires compulsory purchase of a second".

As a child I remember considering the difference between "extra free" and "free" which I used to see on cereal boxes. Sometimes the box claimed "10% free!" but other sneakier boxes would claim "10% extra free!". The latter allows the marketer to quote the same nominal figure for a smaller absolute quantity.

This article includes the assertion:

"Think, for instance, of the common idea that individual recycling can stave off climate change – this in spite of the fact that one hundred companies produce 71 percent of carbon emissions."

Rather shocking if true.

I plead guilty to commenting without reading. Thank you for the gentle reminder!

This reminds me of pitch-drop experiments: https://en.wikipedia.org/wiki/Pitch_drop_experiment

Pitch flows _slowly_. Apparently it is so viscous that at room temperature a suspended blob might release a drop about once a decade or so.

A few university physics departments have had experiments to watch pitch drop running for almost a century.

I tend to agree, I was thinking this as I wrote the above.

My rule of thumb is that if a subject area includes the word "science" in its title, it is less likely to follow the scientific method.

Physicists don't assert that they study "physics science", nor do chemists describe their subject as "chemistry science".

It's only a rule of thumb of course. There are exceptions (computer science, neuroscience, ...) but I think it works in a lot of cases: "social science", "management science", "data science", ...

It's a bit like how if a country includes the word "democratic" in its title, it's less likely to be a real democracy.

In addition to formalising _theorems_, one can aim to formalise _definitions_. See here for some discussion:

https://mathoverflow.net/questions/311071/which-mathematical...

Of course the two are very much intertwined but I think if we're to get serious about formalising mathematics, it would be better to aim to have fully formalised statements of major theorems rather than their proofs for now.

For a long time, I used to dismiss intuitionism but more recently I've come to find it an attractive standpoint.

For one thing, you really only gain by trying to be constructive. If, in some logical system without LEM (law of excluded middle), you cannot find a proof of P without using LEM, you still have a result, namely you can prove LEM -> P. You haven't really lost anything! Furthermore, I have often been surprised just how far you can go without LEM. Very often in fact.

Finding constructive proofs can feel very much akin to removing an unnecessary dependency from a codebase. Also, even if ultimately, you do need LEM somewhere it is often possible to factor it into the "right" place in the proof rather than globally just sticking `LEM ->` at the front of the whole proof.

Also, if you care about, first order logic then in fact you should love intuintionistic logic: it is a finer logic that actually contains first order logic: https://en.wikipedia.org/wiki/Double-negation_translation

Lastly, though I have yet to understand this better, constructive proofs seem to be enjoy better computational properties under Curry-Howard.

And thus obeys good old Mendelian inheritance rules perfectly!

This was news to me and pretty striking:

> The concept of orientability has important implications. Take enantiomers. These chemical compounds have the same chemical structures except for one key difference: they are mirror images of one another. For example, the chemical L-methamphetamine is an ingredient in Vicks inhalers. Its mirror image, D-methamphetamine, is a Class A illegal drug. If we lived in a nonorientable world, these chemicals would be indistinguishable.

It is a Mobius strip.

To convince yourself it might be useful to imagine a point on the surface and imagine tracing it along the strip (avoiding the edges) and seeing if you get back to where your started.

Thanks.

With regard to:

> Can we have a version where one can go far away and come back time-reversed? Or is that excluded by CT=P symmetry breaking?

I don't know. Having mulled these thoughts further after writing the above I'm now more cautious about guessing. Specifically it seems to me that electromagetic charge, weak isospin, isospin etc. are all only globally well-defined provided we have an orientation of spacetime. So it seems to me that if spacetime is not orientable then there's no guarantee that if we send an instance of Wu's experiment off in a spacecraft on a hypothetical orientation-reversing loop then the apparatus will arrive back at earth unchanged: perhaps its electrons are all now positrons etc.

My analogy with the coloured gloves does not permit such a phenomenon because colour is manifestly well-defined. I could make it more elaborate to account for this (e.g., replacing colour with a clockwise/anti-clockwise concept) but I no longer find it useful.

In summary: I revert to my original "no opinion" point of view.