Can I easily prove a contradiction of the form 0=1 in sage?

[Georgi Guninski]

Without doubts, sage and its library have bugs.

Are the bugs "powerful enough" to prove contradiction of the form 0=1?

As a self promotion, around 2008 I proved contradiction in Coq.

[Nils Bruin]

Sagemath is not a proof assistant but computational math software. Any result that sage returns as an answer that provably differs from the intended result can be read as a statement that claims equality between two provably non-equal objects and hence a provable falsehood, all of which are equivalent to the statement "0=1". Note that "intended" and "can be read" leave room for subjectivity: there is probably context required and the assumptions on that may differ between the author and the user. In that sense "misunderstandings" between a computer algebra system and a user are quite possible and happen often.

The more interesting/serious contradictions are generally the ones that persist even after user and system (author?) have established that they actually do agree on the intended meaning and assumptions. With a multi-author system like sagemath, it's quite likely that internal mismatches in assumptions are lurking to produce real bugs.

There's of course a whole bug list for sage with plenty of examples. The symbolic integration system (really just maxima, or giac or sympy or others) is riddled with problems, usually caused by implicit branch cut assumptions. They usually eventually get fixed, but in those cases it usually depends on upstream. And new ones seem to be found at approximately the same rate.

Floats, used as imperfect approximation of reall numnber arithmetic, is inherently inaccurate, so ignoring that mismatch allows easily for 0 == 1 (within epsilon, for sufficiently large epsilon).

Arriving at a (perceived) contradiction in a computational system is of a different nature than in a proof assistant: some parts of sage are in fact documented to produce heuristic (unproven!) results.

That said, bug reports are always welcome. Limited resources for fixing them may cause them to be open for a long time, though.

[Michael Orlitzky]

On Sat, 2023-02-11 at 13:13 +0200, Georgi Guninski wrote:
> Without doubts, sage and its library have bugs.
>
> Are the bugs "powerful enough" to prove contradiction of the form 0=1?
>

In addition to all the good reasons why this might happen: Sage
includes all of python, and python DGAF.