ocfnash

Threading the cores is indeed quite fiddly. I think back in the day, large numbers of seamstresses pivoted into manufacturing core memory!

You can buy core memory kits [1] for adding core memory to an arduino. They only give 8x4 but you could get to "cordmp" with a five-bit encoding ;-)

The vendor, with whom I have absolutely no affiliation except for exchanging a few emails a several years ago, based his kits on a project that I did with a friend a long time ago [2].

It was a fun project that had interesting analog and digital sides to it.

[1] https://www.tindie.com/products/kilpelaj/core-memory-shield-...

[2] https://corememoryshield.com/

I also did pure mathematics, and this summarises my experiences perfectly.

Rumour has it doing a PhD might actually be a rewarding experience in its own right, and not derive its value solely from the possibility of remaining in academia.

Coq uses this notation for (propositional) and and or.

Compiler bugs are indeed pretty frightening. A few years ago I bumped into one in some code that had potential to have a big impact. Unfortunately I am not at liberty to give details about the business setting except to say that we had processes in place that prevented any danger.

In the end I whittled it down to the following tiny C# program:

  namespace UhOh
  {
    internal class Program
    {
      private static void Main()
      {
        System.Console.WriteLine(Test(0, 0));
      }
      private static bool Test(uint a, uint b)
      {
        var b_gte_a = b >= a;
        var b_gt_a = b > a;
        System.Console.WriteLine(b_gte_a);
        return b_gte_a && b_gt_a;
      }
    }
  }

Compiling and running this with Microsoft's .NET stack with versions 4.7.0 and below, the output was incorrectly: "True, True" instead of "True, False". (IIRC, it also had to be a 64-bit Release build.)

The intermediate language was correct; it was a bug in RyuJIT.

Not strictly related but I recall once hearing that Bach may have never heard his Brandenburg concertos performed.

Looking at Wikipedia now I see:

"Because King Frederick William I of Prussia was not a significant patron of the arts, Christian Ludwig seems to have lacked the musicians in his Berlin ensemble to perform the concertos. The full score was left unused in the Margrave's library until his death in 1734 [and] was only rediscovered in the archives of Brandenburg by Siegfried Wilhelm Dehn in 1849"

I have just switched them on and feel very grateful that I can.

I have a little experience of both Coq and Lean and have followed some of the discussion about Lean's handling of quotient types.

I have seen computer scientists emphasise to mathematicians that subject reduction should not be forfeit but I have yet to see a convincing argument/example for why not.

I don't suppose you can elaborate on why this may be / is so crazy, that someone with only a limited understanding of type theory might follow?

I love this write up, and while the solutions discussed are excellent, I think the general-purpose FM Index data structure might work even better. I confess I'd have to read this post more closely to be sure, but I find the FM Index data structure so appealing, I'm always looking for excuses to promote it!

The FM Index is ideally suited to the problem of repeatedly searching a large fixed corpus for many different short substrings, and achieves optimal time complexity: linear in the length of the substring, with excellent constants independent of the length of the corpus (!).

Some years ago undertook a very similar exercise to that of the author except using the leaked Adobe password data rather than the HIBP data, and found the FM Index worked well: http://olivernash.org/2014/01/03/dna-of-a-password-disaster/...

Great job; we need more good citizens like you!

I was unaware that they do at least have the implied 620 figure for the entire US correct, so there is hope that this is just a localised typo.

I can't get over how stunningly-similar this is to the infamous Verizonmath!

Just a moment, 0.72% x 0.03% = 0.0002%, which is about 2 out every 1,000,000.

"The crew went around, climbed to 8500 feet, depressurized the aircraft, opened the cockpit side window and cleaned the windscreen by hand."

I did not miss this statement; for me this does not constitute a recommendation. Indeed I think many of the researchers of whom she is critical could claim that this is what they're doing.

I dare say the author is right on many points but statements like:

"But for all I can tell at this moment in history I am the only physicist who has at least come up with an idea for what to do."

make it hard for me to share her point of view, especially as these ideas are not mentioned.

Note that finite-time singularities for the good old Newtonian n-body problem have been known to exist for quite a while. (See for example [1].)

It's curious to think that a mathematical phenomenon like this can hint at new physics.

[1] Saari, D. and Xia, Z., "Off to Infinity in Finite Time", https://www.ams.org/notices/199505/saari-2.pdf

I find this amusingly reminiscent of the Chinese Room: https://en.wikipedia.org/wiki/Chinese_room

See also Verizon Math [1] for a different failure mode of utility company surcharge billing!

[1] https://www.youtube.com/watch?v=MShv_74FNWU

If anyone even uses it at all!

I have a friend who works in a sales role for IBM. He told me that part of his bonus is contingent on being able to prove that the customer has actually installed the software which they bought.

The policy apparently arose because certain public sector entities had refused to consider new deals since they still hadn't got round to installing the software for which they had paid millions of dollars, years before.

> After reading this, are you really any wiser now on the topic of quotients in Lean?

Only a little but I'm hoping that some weekend reading up on Canonicity and Subject Reduction (now that I know these are the issues at play) will shed some light.

I'm interested in both Lean and Coq but what I'm most excited about is the (Lean-based) Mathlib project.

I can believe that Lean may have made the wrong call on quotients (I guess with `quot.sound`) though I am not qualified to decide. If this is so, I imagine that it will manifest in terms of a natural limit on how far a project like Mathlib can push its borders before it reaches some sort of natural limit (maybe where the complexity of formalising what we want to say dominates the inherent complexity of the statements themselves).

However from what I've seen, Mathlib is by far the most successful formalisation project in terms of what seems to matter most sociologically right now: attractiveness to mathematicians. Whatever its fate, I think it will help make formalisation of mathematics much more mainstream, and will teach us a lot. I still think that a univalent type theory looks like most promising candidate, but we'll have to wait and see.

I strongly recommend reading https://github.com/coq/coq/issues/10871#issuecomment-5404526...

which was written a few hours ago broadly in the vein of Lean vs. Coq, more precisely on the issue of how Lean handles quotients.

According to Chekhov:

"One is shy of asking men under sentence what they have been sentenced for; and in the same way it is awkward to ask very rich people what they want so much money for, why they make such a poor use of their wealth, why they don't give it up, even when they see in it their unhappiness"

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://assets.press.princeton.edu/chapters/gowers/gowers_VII...

Thank you for giving so much of your time, and for your integrity.

You're welcome.

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 pigeon-hole-principle argument in the post this is at most c(m-1)(k-1) cells. Similarly, and still knowing nothing about k except that k-1 < c/n, I count how many cells are row-bad for this value of k and see that it is at most r(n-1)(k-1). Combining these two I know that as long as we have k-1 < r/m and k-1 < c/n the number of cells that are either column-bad or row-bad (or both) is at most:

  * c(m-1)(k-1) + r(n-1)(k-1)

Since I want to be able to conclude that there is a cell that is neither column-bad nor row-bad, and since there are rc cells in total, I then further require that k is such that:

  * c(m-1)(k-1) + r(n-1)(k-1) < rc

(The point is that this is a strict inequality and so there must be a cell that is neither column-bad nor row-bad.)

And then solve this to get the formula for k. Of course when expositing it in the post, I _start_ with the formula which perhaps makes things seem mysterious at first, but I thought was efficient.

Cool!

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 post, here's how the formula arises.

The argument based on counting cells that are either row/column good/bad requires the following of the parameter k:

  1. k-1 < r/m
  2. k-1 < c/n
  3. k−1 < cr/(c(m-1) + r(n-1))

These are equivalent to:

  1. k <= ceil r m
  2. k <= ceil c n
  3. k <= ceil cr (c(m-1) + r(n-1))

And so it is sufficient to have:

  k <= min (ceil r m) (ceil c n) (ceil cr (c(m-1) + r(n-1)))

We can then rearrange this to the headline formula by noting:

  * ceil r m = ceil (cr) (cm)
  * ceil c n = ceil (cr) (mr)

And then simplifying by repeatedly using the fact that for any x, y, z:

  * min (ceil x y) (ceil x z) = ceil x (max y z)

All this is of course in the Coq code. E.g., the last fact mentioned above is here: https://github.com/ocfnash/imo-coq/blob/f6d2e8337fadf00583fd...

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 would be involved in proving something slightly non-trivial but still very elementary. I managed it, but it was _a lot_ more work than expected (results here: https://github.com/ocfnash/imo-coq).

Partly based on this exercise, I think that while it is possible that mathematics may go the way of chess, so to speak, it is a lot more distant than the ten years mentioned in this article.

I strongly support, very much hope, and even expect, that the use of proof assistants may become mainstream in mathematics within a generation or so but I think it is impossible to guess the exact role they will play accurately.

Thanks, that was very sloppy of me!