Search All of the Math Forum:
Views expressed in these public forums are not endorsed by
NCTM or The Math Forum.



Re: Formal Proof of CantorBernsteinSchroeder Theorem using DC Proof 2.0
Posted:
Jun 15, 2013 11:44 AM


On Jun 15, 2:57 am, Jan Burse <janbu...@fastmail.fm> wrote: > Dan Christensen schrieb: > > > Full text at:http://dcproof.com/CBS.htm From the informal > > introduction: > > > THEOREM (CantorBernsteinSchroeder): > > 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 fixedpoint 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.
Dan Download my DC Proof 2.0 software at http://www.dcproof.com



