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).

Love using mathematics to prove weird facts like this.

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!