proof by example

Stream: general

[Johan Commelin]

I think the following slides may be of interest to many people on this Zulip: https://math.bu.edu/people/matschke/slides-proofs-by-example.pdf

[Johan Commelin]

Proving a theorem by showing one example. "All primes are even. Example: 2. QED."

[Martin Dvořák]

I don't get it. Is the method supposed to be sound for logical reasons? Or is it just that the probability of proving an incorrect theorem is zero?

[Johan Commelin]

It's logically sound.

[Martin Dvořák]

Wow! I should look at it again. It sound very very interesting!

[Scott Morrison]

I do love the Schwartz-Zippel lemma, and have a paper with some "probably true" theorems proved using it.

[Bolton Bailey]

@Scott Morrison Sounds cool. I would be interested in a link/title.

[Scott Morrison]

@Bolton Bailey, it's Lemma 6.10 of https://arxiv.org/pdf/1501.06869.pdf. I'd actually forgotten; the result that uses the Schwartz-Zippel lemma we actually give two proofs: one that it only true with probability 1-10^{-500}, and a more involved but unconditional proof. It's a bit of a strange paper, but is actually fairly self-contained if you skip the parts of the introduction that talk about pivotal categories. Besides that, it's just about planar trivalent graphs. (And, weirdly enough, makes use of grobner bases and elliptic curves along the way.)

[Bolton Bailey]

Thanks. I ask because I have become interested recently in what you might call probabilistic proofs like this that only hold with high probability over some random choice of the verifier and the obstacles to formalizing these in a proof assistant.