The Math Forum

Search All of the Math Forum:

Views expressed in these public forums are not endorsed by NCTM or The Math Forum.

Math Forum » Discussions » sci.math.* » sci.math

Notice: We are no longer accepting new posts, but the forums will continue to be readable.

Topic: Formal Proof of Cantor-Bernstein-Schroeder Theorem using DC Proof 2.0
Replies: 2   Last Post: Jun 15, 2013 11:44 AM

Advanced Search

Back to Topic List Back to Topic List Jump to Tree View Jump to Tree View   Messages: [ Previous | Next ]
Dan Christensen

Posts: 8,219
Registered: 7/9/08
Re: Formal Proof of Cantor-Bernstein-Schroeder Theorem using DC Proof 2.0
Posted: Jun 15, 2013 11:44 AM
  Click to see the message monospaced in plain text Plain Text   Click to reply to this topic Reply

On Jun 15, 2:57 am, Jan Burse <> wrote:
> Dan Christensen schrieb:

> > Full text at: From the informal
> > introduction:

> > THEOREM (Cantor-Bernstein-Schroeder):
> gr8 work! Congratulations.

Thank you.

> The proof has >1000 lines, could it be made shorter?

Currently at 1,262 lines, it could be made a little shorter. I might
be able to get it under 1000. I will be going through the proof at a
later date to see if I can make some improvements.

> When I was googling I found different operators used
> to yield a fixpoint. The one you were using is found
> on the french wikipedia side, another one is shown
> on the german wikipedia side.

I have a proof of the fixed-point theorem as well (241 lines). I hope
to be releasing it, along with a collection of proofs on orders of
infinity, with an update of my program this summer.

Download my DC Proof 2.0 software at

Point your RSS reader here for a feed of the latest messages in this topic.

[Privacy Policy] [Terms of Use]

© The Math Forum at NCTM 1994-2018. All Rights Reserved.