Schlagwort-Archiv: Mathematik


Is it still a proof if it takes 4 minutes on a 4 GHz 12-core CPU?

Aus den Takten.

Of the New Day is a song of rebirth, emerging from darkness. It sounds deceptively simple, a recognisably atypical Porcupine Tree ballad. That is until you realise that the length of the bars is constantly changing, flipping between bars of regular 4/4 time to 3/4, to 5/4 to 6/4, 11/4, so that the track never settles into any steady time. It’s what PT can sometimes do really well, come up with a basic idea that’s almost intellectual or mathematical, but carry it off in a way that sounds completely natural and accessible.

Steven Wilson


Hey! I heard that Lean thinks 1/0 = 0. Is that true?

Yes. So do Coq and Agda and many other theorem provers.


But doesn’t that lead to confusion?

It certainly seems to lead to confusion on Twitter. But it doesn’t lead to confusion when doing mathematics in a theorem prover. Mathematicians don’t divide by 0 and hence in practice they never notice the difference between real.div and mathematical division (for which 1/0 is undefined). Indeed, if a mathematician is asking what Lean thinks 1/0 is, one might ask the mathematician why they are even asking, because as we all know, dividing by 0 is not allowed in mathematics, and hence this cannot be relevant to their work.

Xena: Division by zero in type theory: a FAQ

Nice but late.

“But there is no honor in elegantly proving a theorem in 1672 that some Scotsman proved barbarously in 1671!”

Neal Stephenson: Quicksilver

No arrows, not even objects.

Am I the only one who annoyed by "functor" in Prolog?

Teilen mit Rest.

Bistromathics itself is simply a revolutionary new way of understanding the behaviour of numbers.

Douglas Adams: The Restaurant at the End of the Universe


The dangerous bend or caution symbol ☡ [...] was created by the Nicolas Bourbaki group of mathematicians and appears in the margins of mathematics books written by the group. It resembles a road sign that indicates a "dangerous bend" in the road ahead, and is used to mark passages tricky on a first reading or with an especially difficult argument.

Wikipedia: Bourbaki dangerous bend symbol

Ältere Beiträge «