alimw

> Would the US kindly send money? Again. And again.

Where is this money?? Still waiting for mine!

I dunno, my local (council-affiliated "Better" brand) gym claims exactly that in its advertising — that you pay by the month with no cancellation fee — but it turns out when you go to cancel that they have already laid claim to the next month's payment too and there's not a damn thing you can do about it. On that day I certainly wished I had it on its own special account that I could just close.

Is the error to assume that any logic at all might apply to this matter? "Whereof one cannot speak, thereof one must be silent."

On the other hand, if more innocent people lacked the awareness to avoid dodgy areas then they probably wouldn't be so dodgy!

Mochizuki is unenthusiastic.

[1] Section 1.12 of https://www.kurims.kyoto-u.ac.jp/~motizuki/Essential%20Logic....

Oops! I checked the spec and it's supposed do something more like this:

  def f (n : Nat) : String :=
    Option.getD
      (Option.merge String.append
        (if n % 3 = 0 then "Fizz" else none)
        (if n % 5 = 0 then "Buzz" else none))
      (toString n)

  #eval List.map (fun k => f (k + 1)) (List.range 100)

  theorem poop (n : Nat) :
      f n = "FizzBuzz" ∨ f n = "Fizz" ∨ f n = "Buzz" ∨ f n = toString n := by
    unfold f
    split <;> split
    · exact Or.inl rfl
    · exact Or.inr (Or.inl rfl)
    · exact Or.inr (Or.inr (Or.inl rfl))
    · exact Or.inr (Or.inr (Or.inr rfl))

Yes split_ifs is in Mathlib so I have replaced it with split (twice) which is in Core. I believe there is also an intermediate level Std. I'm not sure why you'd want to avoid Mathlib but I daresay it's possible for many types of problem.

Sure!

  def f (n : Nat) : String :=
    String.append
      (if n % 3 = 0 then "Fizz" else "")
      (if n % 5 = 0 then "Buzz" else "")

  #eval List.map f (List.range 100)

  theorem poop (n : Nat) : f n = "FizzBuzz" ∨ f n = "Fizz" ∨ f n = "Buzz" ∨ f n = "" := by
    unfold f
    split <;> split
    · exact Or.inl rfl
    · exact Or.inr (Or.inl rfl)
    · exact Or.inr (Or.inr (Or.inl rfl))
    · exact Or.inr (Or.inr (Or.inr rfl))

"So what might have caused this strange new syndrome in our trading platform?" "Perhaps one of the market participants was doing something different?" "Nope."

Then literally two hours of me stumbling through possible technical issues to do with the internals of a system I had never seen. Even though I had thought I was being considered for my maths rather than my computer skills.

"Well just so you know, it turned out that one of the guys trading on the platform was doing something different." Laughing politely, "but you told me...". "Oh well no that's not what I would consider a market participant."

I call my laughter polite but I suspect it had an edge to it. Anyway he immediately walked me out saying, "we'll send you feedback." The feedback was that I had asked for too much money. (I hadn't asked for anything.)

They iterate f where f(z) = (a₀ + a₁ z ź + a₂ Re(zⁿ) + a₃ i) z + a₄ źⁿ⁻¹. You can easily check that f(z exp(i 2 π / n)) = exp(i 2 π / n) f(z).

All of these are aperiodic; it says as much in the first paragraph. Are you talking about the rotational symmetry?

"... please use the original title, unless it is misleading or linkbait; don't editorialize." https://news.ycombinator.com/newsguidelines.html

Is this a quality article? It starts badly:

> ... elevation of the land is equal to the value of the function (the “profit”) at that particular spot. Gradient descent searches for the function’s local minimum ...

Just remind yourself that these people have probably thought harder about their problem domains than you have.

"In Intellectual Mathematics a topic is introduced only when the student can be convinced of the value of doing so."

If I understand this correctly, you cannot bend the approach to the teaching of any particular topic (e.g. what's in your son's homework this week). Rather you would have to bite the bullet and teach your own parallel course, abandoning the school curriculum to the teachers.

I guess this is the banal reason why most conspiracy theories take off. They "sound interesting".

Now you can have an unelected technocrat somewhere in the UK write the standards for your new toaster. Or more likely it'll just be forgotten in the bonfire of regulations and you'll end up dead on your kitchen floor in a warm pool of butter.

> ...the only scenario that really makes sense for Russia...

Dictatorships don't come without an internal power struggle. Your logic depends on a view of Russia as a single self-serving entity.

"Just asking questions" huh? Well unless they are heading somewhere (like towards answers), questions by themselves are not worth a damn. But perhaps you really are trying to post signs to some conclusion you regard as natural? If so just come out with it, because I for one can't guess.

This seems about right. Work with pennies why not. My very basic test suggests that 1 - 2^(-53) is distinct from 1 in double-land. So if x is the total number of pennies and 2^(-53) * x < 0.5 I can't see why any problem would arise. That's assuming a proper rounding back to integers at the end.

> though I'm not sure anyone ever used an interactive theorem prover to show a conjecture they did not know was true

The Liquid Tensor Experiment [1] formalised a proof that the author himself found sufficiently complicated to have doubts about. And at a very different level, I myself began to formalise a proof [2] while it still had at least one hole in it. I was fortunate it turned out to be true!

[1] https://leanprover-community.github.io/blog/posts/lte-final/ [2] https://github.com/agjftucker/exists-unique

There are some Lockhart books mentioned on this page.

The MacBook doesn't have ctrl on the right! But I've done my best to follow this advice by making right-opt into ctrl and right-cmd into meta.

The word "original" does not appear so I don't know why you've put it in quotes. Indeed you don't have to read very far down the article to find acknowledgement that something similar had been done centuries earlier in China.

Edit: I see the headline (probably written by someone other than the author) says they "invented banking". There are of course many claims to that dubious honour!

In fairness to the article, it does go on to say

> Sanskrit, although not widely spoken, is the sacred language of Hinduism and has been used in India's science, philosophy, poetry and other secular literature over the centuries.

It's very hard to believe that an actual human wrote the responses I've had from Camden Council over the last couple of months.

In France taxes have made gasoline about twice the price it is in the US, which may explain the increased sensitivity. That fact would also seem to contradict this article summary (I haven't read the article itself) and its suggestion that higher taxes are politically impossible in the long term?

"Rogan did not name the school, and his publicist did not respond to a request for comment."

1. If I comment to correct a minor detail in someone's question, and they don't bother either to respond or to fix it, then I know it's not going to be worth going to the effort of giving a full answer.

Mathematical claims may be formalised in a proof assistant.