ocfnash

12 ms·

1. 61.▲
   by ocfnash 7y ago

   Agreed. For what it's worth I think Atiyah's advice on writing mathematical papers, written for the Princeton Companion to Mathematics, is well worth a look. See "Style", starting on page 4 of this PDF: http:/&#x2F
2. 62.▲
   by ocfnash 7y ago

   Thank you for giving so much of your time, and for your integrity.
3. 63.▲
   by ocfnash 7y ago

   You're welcome.
4. 64.▲
   by ocfnash 7y ago

   https://outline.com/PPAFw4
5. 65.▲
   by ocfnash 7y ago

   Oh I see. Here's how I got there (still using the terminology / notation of my original post). Without knowing anything about k except that k-1 < r/m, I counted how many cells are column-bad for this value of k. By the pig
6. 66.▲
   by ocfnash 7y ago

   Cool!
7. 67.▲
   by ocfnash 7y ago

   I presume you've been looking at my presentation here http://olivernash.org/2019/07/06/coq-imo/index.html which I confess is quite concise; apologies if it is too terse. Reusing the notation of my p
8. 68.▲
   by ocfnash 7y ago

   I've been following Buzzard's evangelism of proof assistants for some time. A few months ago I decided to try formalising some old mathematics olympiad problems in Coq. Part of my motivation was to get a sense for how much work wo
9. 69.▲
   by ocfnash 7y ago

   Thanks, that was very sloppy of me!
10. 70.▲
    by ocfnash 7y ago

    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,
11. 71.▲
    by ocfnash 7y ago

    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://ar
12. 72.▲
    by ocfnash 7y ago

    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 cubica
13. 73.▲
    David Spiegelhalter's Cambridge Coincidences(understandinguncertainty.org)

    1 points by ocfnash 7y ago|0 comments
14. 74.▲
    Abraham–Minkowski Controversy(en.wikipedia.org)

    7 points by ocfnash 7y ago|0 comments
15. 75.▲
    by ocfnash 7y ago

    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
16. 76.▲
    by ocfnash 7y ago

    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` con
17. 77.▲
    by ocfnash 7y ago

    As well as a new sort, SProp! https://coq.github.io/doc/v8.10/refman/changes.html#version-...
18. 78.▲
    by ocfnash 7y ago

    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"
19. 79.▲
    by ocfnash 7y ago

    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 re
20. 80.▲
    by ocfnash 7y ago

    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 s
21. 81.▲
    by ocfnash 7y ago

    I am a geometer by training.
22. 82.▲
    by ocfnash 7y ago

    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 int
23. 83.▲
    by ocfnash 7y ago

    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
24. 84.▲
    by ocfnash 7y ago

    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) &gt
25. 85.▲
    by ocfnash 7y ago

    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:
26. 86.▲
    by ocfnash 8y ago

    >> 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
27. 87.▲
    by ocfnash 8y ago

    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
28. 88.▲
    Vulnerabilities in Medtronic's implanted heart defibrillators(theregister.co.uk)

    1 points by ocfnash 8y ago|0 comments
29. 89.▲
    by ocfnash 8y ago

    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
30. 90.▲
    by ocfnash 8y ago

    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 agr