In which we go deep down the grammatical rabbit hole, and unlock the infinite buffalo sentence.

This guy really likes recursion.

In nonmonotonic reasoning, the Nixon diamond is a scenario in which default assumptions lead to mutually inconsistent conclusions.

This is a fun example in logic I recalled recently.

Richard Nixon is both a Quaker and a Republican

Mathematicians manipulate sets with confidence almost every day, rarely making mistakes. Few of us, however, could accurately quote what are often referred to as “the” axioms of set theory. This suggests that we all carry around with us, perhaps subconsciously, a reliable body of operating principles for manipulating sets. What if we were to take some of those principles and adopt them as our axioms instead? The message of this article is that this can be done, in a simple, practical way (due to Lawvere). The resulting axioms are ten thoroughly mundane statements about sets.

This is an expository article for a general mathematical readership.

A nice read, although it definitely gets a bit difficult towards the end.

via: https://topos.institute/blog/2025-07-13-liberating-synthetic-quasi-coherence-from-forcing/

via: https://buttondown.com/hillelwayne/archive/logic-for-programmers-extra-credits/

Partial orderings are a useful concept that would have taken too many pages in the book, so I’m putting it here.

via: https://buttondown.com/hillelwayne/archive/logic-for-programmers-extra-credits/

We establish new, yet intimate relationships between the 2-adic integers /sub 2/Z from arithmetics and digital circuits, both finite and infinite, from electronics.

VERY interesting paper! Sadly didn’t answer all my questions about 2-adic circuits, but it did answer quite a lot.

see: https://www.di.ens.fr/~jv/HomePage/pdf/cirnum.pdf

see: https://scispace.com/pdf/on-circuits-and-numbers-3du2olohli.pdf

via: https://en.wikipedia.org/wiki/Two%27s_complement#Two’s_complement_and_2-adic_numbers

This talk will focus on one such verification approach that takes as input a design under verification (DUV), modest architect-friendly DUV metadata, and a HW-SW contract. The approach automatically generates many simple formal properties that provably compose to imply the contract, and then evaluates them against the DUV to assess contract compliance. The enabling insight is that many important HW-SW contracts decompose into instantiations of a small, finite set of property templates, fillable automatically from the supplied metadata or from the results of evaluating other generated properties. This verification approach eliminates manual property writing, targets full HW-SW contracts rather than coverage metrics, and yields properties simple enough that commercial formal model checkers can produce unbounded proofs for most, even on complex designs.

One consequence of this is that checking whether assumptions hold is a different problem from verifying that your code works given the assumptions. Like to make sure “all unsafe blocks are safe” can’t use the Rust compiler, you need a second tool like Miri. I wonder if checking assumptions is, in practice, generally more difficult than checking everything else.

A formal type of proof most frequently encountered in elementary geometry courses in which known or derived statements are written in the left column, and the reason that each statement is known or valid is written next to it in the right column. The proof then proceeds from the known facts to the theorem to be demonstrated. […] However, this form of proof is virtually never used by practicing mathematicians because its confining and verbose format render it of very limited utility to any but the most simple of theorems.

Hmm, maybe this is why people don’t like Lean LOL.

Kurt Gödel discovered a solution to General Relativity that allows time travel without any exotic physics, revealing that the theory doesn’t actually guarantee a consistent chain of cause and effect . His “Gödel universe” shows that under certain conditions, the structure of spacetime itself can loop back on itself—blurring the line between past and future and exposing a deep limitation in our understanding of reality.

The GÖAT!

Buy Lets Go! by Francis McCabe (Paperback) online at Lulu. Visit the Lulu Marketplace for product details, ratings, and reviews.

When “what CAN happen” is as important as “what SHOULD happen”

Can’t fully understand because there are no words, but the author looks to be making a very neat connection between coalgebras and the executions (here “traces”) of transition systems. Became aware of her work through Adjoint School 2026.

via: https://www.cs.uni-salzburg.at/~anas/talks.html

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.

I think this is the first highly technical Topos Institute blog post where I walked away and felt like I understood everything I was meant to understand. Heck yeah.

I’ve been thinking about very similar ideas for the better part of a year now; excited to see there’s good work regarding this.

No matter how hard we try to axiomatise mathematics, there will always be strong, independent propositions that don’t need no proofs… but how do we show that a proposition can’t be proven nor disproven?

Nice set of videos on the theory of ordinals and their application to Goldstein sequences.

Ever feel like the mathematics you’re learning doesn’t make any sense to you? Good. In a way, it would’ve been worse if you thought it did make sense.