Schlagwort-Archiv: Mathematik

Lean.

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

Leanorris.

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 «