The article considers structuralism as a philosophy of mathematics, as based on the commonly accepted explicit mathematical concept of a structure. Such a structure consists of a set with specified functions and relations satisfying specified axioms, which describe the type of the structure. Examples of such structures such as groups and spaces, are described. The viewpoint is now dominant in organizing much of mathematics, but does not cover all mathematics, in particular most applications. It does not explain why certain structures are dominant, not why the same mathematical structure can have so many different and protean realizations. ‘structure’ is just one part of the full situation, which must somehow connect the ideal structures with their varied examples.

Very nice philosophy paper by one of the progenitors of category theory on structure. The idea to show a correspondence between Bourbaki and category theory seems like a nice grad school project.

Very slick technique.

This is the kind of mathematics I was put on this earth to do. The equation explorer is also just a genuinely useful tool for looking up equations; did so earlier this year as part of preparations for a lecture I gave.

A counterexample is any exception to a generalization. Counterexamples  are often used in science (and philosophy), as a means to setting boundaries. In mathematics at large,  well-chosen counterexamples may  bound possible theorems, disprove certain conjectures. This conspectus is (mostly) meant to gather and share counterexample book references (on algebra, analysis, calculus, logic, philosophy, probability, statistics, topology).

“Correct” doesn’t mean “correct” when correctly using “correct”

via: https://buttondown.com/hillelwayne/archive/three-ways-formally-verified-code-can-go-wrong-in/

We programmers need all the help we can get, and we should never assume otherwise. Careful design is great. Testing is great. Formal methods are great. Code reviews are great. Static analysis is great. But none of these things alone are sufficient to eliminate bugs: They will always be with us. A bug can exist for half a century despite our best efforts to exterminate it. We must program carefully, defensively, and remain ever vigilant.

via: https://lukeplant.me.uk/blog/posts/breaking-provably-correct-leftpad/ via: https://buttondown.com/hillelwayne/archive/three-ways-formally-verified-code-can-go-wrong-in/

One often hears it said that “absence of evidence is not evidence of absence”. For example, if you excavate some fossil sauropods and they don’t have preserved feathers, that not evidence that sauropods didn’t have feathers. Oh yes it is.

In this cross-over episode between the Main Sequence and Tom Academy, we see what it would take to prove that you can’t do what you already thought you couldn’t do, and learn about Tom’s prurient interest in Platonic horrors. Yes, the whole 80 minutes is about cubes and their relatives.

Love using mathematics to prove weird facts like this.

This is how we do math in the 21st century.

So when you see a no-go theorem that’s being given a very broad interpretation, you may do well to ask whether there is, after all, a way to get around the theorem, by achieving what the theorem is informally understood to preclude without doing what the theorem formally precludes.

Gödel’s Incompleteness Theorem explained with Pen, Paper & Lean (the proof assistant)

Our goal is to carry out some simple examples of program verification – i.e., to use the precise definition of Imp to prove formally that particular programs satisfy particular specifications of their behavior. We’ll develop a reasoning system called Floyd-Hoare Logic – often shortened to just Hoare Logic – in which each of the syntactic constructs of Imp is equipped with a generic “proof rule” that can be used to reason compositionally about the correctness of programs involving this construct.

One of the many exciting new features in the upcoming Lean 4.22 release is a preview of the new verification infrastructure for proving properties of imperative programs. In this post, I’ll take a first look at this feature, show a simple example of what it can do, and compare it to similar tools.

Excellent stuff!