[phaemon]

> "So this means: it has a divisor not in the initial primes (actually, I think it must have two). But why should it be prime?"

Ok, this is the heart of the issue. If the new number is a prime, all is well and good, but if the number isn't prime, why should it's divisors be?

The simple answer is: they don't have to be. If you have divisors that aren't prime, then keep dividing till you hit some that are. The definition of a prime number is one that can only be divided by itself, so for any non-prime number, you must be able to keep finding factors until they're all prime!

Let's take an example. Our list of primes is {5,7} which are nice small numbers to use. By following the rule of "multiply and add 1" we get:

    5 * 7 + 1 = 36.

Ok, so let's break 36 down. We get:

    36 = 2 * 18

Right, well, 2 isn't on our list, but let's face it: 2 isn't a real prime. None of the other primes like it. It's even. Nor is 18 on our list, but that's not prime (and that was your objection before), so let's break 18 down.

    36 = 2 * 2 * 9

Well, that's a bit better. We have another unpopular 2, but we also got a 9, and even though 9 isn't prime, it's probably primier than 2 is. Continue on:

    36 = 2 * 2 * 3 * 3

There we go. Now we actually have a proper prime number, "3", that we can add to our list.

And you see (I hope) that none of these numbers could possibly be on our original list, because all the numbers already on that list give a remainder of "1" when we divide "36". Yet we must, inevitably, hit a prime number because we just keep dividing till we do!

[lutusp]

> Right, well, 2 isn't on our list, but let's face it: 2 isn't a real prime.

I can't tell whether you're taking this position or ridiculing it, but if 2 isn't accepted as a prime number, this would falsify the Fundamental Theorem of Arithmetic for all even numbers.

http://en.wikipedia.org/wiki/Fundamental_theorem_of_arithmet...

Quote: "In number theory, the fundamental theorem of arithmetic, also called the unique factorization theorem or the unique-prime-factorization theorem, states that every integer greater than 1[3] either is prime itself or is the product of prime numbers ..."

If your purpose was satire, then perhaps this post will inform other readers who may not detect your satirical intent.

[phaemon]

As you suspected, it was intended as a joke.

The other primes do, in fact, quite like 2, and 9 is not in any way primier than 2 despite my previous assertion.

EDIT: Actually, there was a real point to ignoring 2, and it was just so I could carry on breaking down the factors as that seemed to be the bit that hyp0 was having trouble with. Perhaps it did confuse more than enlighten. I'm not sure.

[hyp0]

Yes, that's what I meant by my third paragraph (the one following the question you quoted, answering it).

[phaemon]

Ok, so do you see now why the prime divisors of 18 (in that particular case) can't be on the original list, because otherwise they would also divide 36 (and we know they leave remainder 1). And therefore we must hit some primes that aren't on the original list (in fact, none of the primes we hit can be on the original list).

In short, do you feel comfortable with the proof now?

[hyp0]

Don't you think that's covered by the following?

> [...] divisors which in turn are either prime or have divisors etc. None of these divisors are an initial prime, because then they would also be divisors of p+1

Let me put it this way: I think I'd score 100% on an exam on this, but I don't "get" it.

The divisors of 18 are also divisors of 36, because 36 = 18 * 2. Could use a theorem here, that a divisor of a divisor (of x) is also a divisor (of x).

A way to put it: p+1 can't be divided by any initial primes; and, if we keep dividing divisors, we eventually can't divide any more, and that's the definition of prime (indivisible "atoms"!).

I like seeing the overall process as: each time you find a new prime, it could fill in a gap between primes in the list, or be greater than any of them. Or, be smaller than any of them:

  3*5 +1 = 16    -> 2

[BTW I can't tell if this is guaranteed to find all primes (though I conject it does); but that's OK, as the proof doesn't claim that, only that it always finds one more prime. Maybe there are some sets of initial primes that will always miss some prime/s - a proof of that might go deep.]

  \tangent

Regarding code vs proof, I like what rspeer/tjgq said on abstractions/theorems - accepting a lower level, and working above that. But code is different, in that its purpose is to do something. If it does that, then it "works" in a practical sense (even if buggy). Thus, I can tell that the lower levels are working well enough, for my purposes.

In contrast, the purpose of a proof is to convince me that it's true. Sure, if I accept the theorems, and I accept the proof given those theorems, then I accept the proof. But this means that in order to be convinced that the proof is true, I have to be convinced of all the levels.

The difference isn't code vs proof in themselves, but in their purpose. I demand a lot more of a proof!

  \idea

(Not Curry-Howard, but...) Maybe I should make a programming language for making convincing proofs that does work like code (unlike coq, which aims more at professional mathematicians). It can be lacking features, like handling infinity; it can be slow.

You "run" the proof to check it; you can "step into" theorems (like a debugger or some theorem websites which hyperlink them), or collapse/hide them.

It would be set-based, and so fundamental in that sense. I'm not sure if it would actually create sets and operate like an algorithm on them; or if it would use theorems about sets. I think the latter is necessary for "proof", but it wouldn't be as convincing... Generating examples would be helpful, to show it "working". hmmm... some proofs work kind of "by example", but with variables. What makes it a "proof" is that it works for the full range of values needed. So emphasising that approach might help.

The language would enable you to divide up an issue into possibilities in various ways, and automatically check that each limb is addressed (this is the basis of proof to my mind: you divide up the issue, and show that this covers all possibilities; then handle each limb. e.g. the predicate "is prime" or not). You can nest divisions. Not far from pattern matching, as in ML/haskell.

The actual proof part would be chains of implies: given x, y is true. These can be theorems/libraries: in the stdlib, or a third-party library, or your own "app" (or, the language's built-in axioms and theorems). So you can't just magically go from one step to the next; you have to specify a theorem for that step (call it). Perhaps the most basic ones would be implicit (like implicit casts), to avoid too much tedium. You can then "step into" these calls, or collapse them. Actually, just defining a new theorem is a way to collapse it (debugger "step into", collapsable tree and hyperlinks are just UI choices - vim ^] is another way to navigate calls, conceptually expanding/collapsing).

A key convention here would be that it's not enough to be correct if it's a complex, confusing, tedious "spaghetti proof". You want clear proofs, that ideally formalize intuitive notions. You build libraries that might not be the most concise, but that give you theorems that "make sense" and are useful for building convincing proofs. Libraries can compete etc for the "best" formalisms.

That is: unlike mathematicians, we don't aim at brevity or elegance, but at being convincing, intuitive, easy to understand. Accessible to ordinary people - pop-proofs, like pop-science, pop-psychology, pop-art etc. And I wouldn't be doing this magnanimously, for the poor ignorant masses, but because I need it myself!

It wouldn't be doing anything very clever, just easing the cognitive burden of complex proofs:

record the detail (just document management alone is helpful); hide/reveal one part at a time; automatic checks; affordances whose existance guides you to sensible operations (e.g. divide it up; implies; implicit theorems). There's also the fundamental aid of helping you formally defining the problem in the first place... which can be hardest part of proving it.

  \implementation

Thinking how this would actually work. Each line would be an expression following from the previous expression + a theorem. Conceptually, we are transforming the expression in each step.

In a way this is bad, because you're having to explicitly type so much... in a regular program, you just call a function, and you don't need to show the returned result - it's hidden in the execution. We could do that here, but it would be less clear:

This unclear version would look like: a starting expression, then a sequence of transformation theorems/calls (specifying exactly how they're applied). You'd run it to see the sequence of expressions as it was transformed.

A problem is we'd have to specify tediously what we want. For example, given expression a and b and operator ->, it couldn't know whether we want a (or b) - or something else, because many things are implied. So the operations would to be very precise. Like, extract the first operand; extract the second operand. It's similar for trivial operations like commut/associate a and b and c - we must specify precisely which ones to permute. I guess we could have a "permute" rule that operates at a higher level (i.e. actually a theorem...); or even have an "operator" that specifies the operation via the result... so it's no longer really an operator, but a kind of declarative system that I first mentioned.

One option is some "live" editing environment, so we can get the result of the call automatically. A couple of problems: we might not want the literal result, but an implicitly transformed version (e.g. trivially, like re-ordered terms). We'd also have to specify exactly how the theorem was applied - this might be a problem anyway (if it's to be automated).

I'm thinking that the engine works out how to apply the theorem to transform the starting expression into the resulting expression... but that might be too hard; we may need to tell it exactly how to apply it (like positional arguments to a function).

But... I guess it might even be a good rule of thumb, that if we can't mechanically work out what the step is, it's too complex! And if the user really wants it as a single step, they can write a theorem, that breaks it down enough into smaller steps simple enough for the compiler to understand. That seems to serve our goal, of convincing... at least, in principle. It might be tedious in practice.

For implict theorems, it seems commutativity/associativity would be OK; maybe distributivity - but if a big change, might be hard to follow.

Inference: We might allow any theorem to be implicit, provided the engine can infer not just how to apply the theorem, but what the theorem actually is (i.e. find some way to justify the step). This is quickly heading towards an automatic theorem prover, at least for very simple proofs. A problem with this is that the step might be less clear - that is, although the engine can work it out, the user might not be able to. This could easily happen in practice, even if the engine isn't very clever, by it having a library of very advanced theorems that the user doesn't even know about (this might be partially mitigated in an active environment, where the engine suggests the theorem - like a tooltip, google suggest, autocompletion).

Two kinds of transform, equational (an equal expression) and implies (not equal, but some aspect of it e.g. a and b -> a)

[hyp0]

EDIT one danger with a library is it might have a theorem stronger than what you're trying to prove (and that you aren't convinced yet by). If it's applied automatically, it's not a convincing proof. (And the purpose here is to be convincing, not just to be correct).

The easy answer is for the user to only allow libraries that they've accepted.

I was thinking we might have an automatic check, that we never use a theorem which is stronger than the whole thing we're trying to prove - that is, which implies our whole proof). But that seems hard to check automatically (maybe undecidable in general).