Anyone is free to include in their math paper a statement of the shape "Computer checkable proofs of Theorems 1 and 2, and Lemmas 3-6, are available at the URL math.foo.edu/~baker/paper7.txt" . Maybe noone has thought to do it yet. An extreme endpoint of checking is verifying a Mersenne Prime, where you pretty much have to repeat the LL test. But of course they do that anyway. A checkable proof of the Odd Order Theorem could be very useful, since it would likely result in the discovery and repair of some minor errors. But it seems unlikely that much of our edifice is built on wrong stuff, so making checks required seems extreme. And it could chase the non-detail-oriented out of the profession. (Or perhaps they'd make their grad students do it. Hmmm. Would the 8th Amendment apply?) ---- Sudoku: I ran across a moral dilemma in a Sudoku last night: Can I use the uniqueness of the solution to exclude some lines of argument? My partial solution looked like this: Z - Z | * * * | * * * x - x | * * * | * * * x - x | * * * | * * * --------------------- x - x | * * * | * * * x x ? | * * * | * * * x - x | * * * | * * * --------------------- x x x | * * * | * * * x x x | * * * | * * * Z x Z | * * * | * * * x is a known value, - is an empty cell (so far), * could be either. I knew that the left column Z,Z values had to be 2,6 in some order, and the third column Z,?,Z values had to be 2,3,6 in some order. I observed that, if I assigned 3 to the ?, that the Zs could be either 2,6 and 6,2, or vice versa. If one solution worked, the other would also, since all the puzzle constraints on uniqueness etc. would be satisfied in either case. Hence, if I used my meta-knowledge of a unique solution, I could exclude the value 3 in the ? cell. Dilemma: Is this fair? In a race, there's no way to exclude the inference; and we used to do similar things on multiple choice tests. But for self solving, should the conclusion be allowed? Rich