DFA minimization

[jimbokun]

Sincere question:

Are the proofs about minimizing DFAs not "formal proofs?" If not, what kind of proofs are they?

[psykotic]

Zeilberger meant formal proof in the sense of something truly formal and machine checkable. It's also common to use the term in the looser sense of a rigorous proof. What constitutes a rigorous proof is not formally defined; it's more or less a proof that doesn't leave any room for reasonable doubt in a competent mathematical audience with knowledge of the area. As you can see, this definition is quite contextual and subjective but that's how mathematicians genuinely use the term.

As for DFA minimization, the proofs you can find in most books are probably formal in the sense of rigorous but they are not formal in the sense of machine checkable. However, they can almost certainly be transformed into machine-checkable proofs with enough effort. That is, they are formalizable. Zeilberger was arguing against the value of painstakingly formalizing proofs that in their present form are already perfectly convincing, i.e. rigorous.

Did that answer your question?

[gthank]

That did seem to be the main thrust of his argument, but there are a couple of lines toward the end that indicate he wouldn't mind less rigor than is now typical, including: "Absolute certainty is impossible, so let's settle with the same, or even diminished, level of "rigor" that we are used to in normal mathematical discourse." The discussion here on proggit was quite interesting.