Are results found of an Elliptic Curve by SageMathCell proven (does there exists no more solutions)?

The documentation of integral_points cites the algorithm found in

Henri Cohen, Number Theory, Vol. I: Tools and Diophantine Equations. GTM 239, Springer, 2007.

You can read the implementation e.g. by entering E.integral_points?? into a SageMath session.

The algorithm finds all the integral points, but it depends crucially on having computed the Mordell-Weil group.

On this topic, the documentation reads:

mw_base - list of EllipticCurvePoint generating the Mordell-Weil group of E (default: ‘auto’ - calls self.gens())

Note: The complexity increases exponentially in the rank of curve E. The computation time (but not the output!) depends on the Mordell-Weil basis. If mw_base is given but is not a basis for the Mordell-Weil group (modulo torsion), integral points which are not in the subgroup generated by the given points will almost certainly not be listed.

In turn, the documentation of gens(), about its optional argument proof, says:

proof – bool or None (default None), see proof.elliptic_curve or sage.structure.proof

Finally, the documentation of proof.elliptic_curve states:

Controls the default proof strategy for elliptic curve algorithms.

Calling it:

sage: proof.elliptic_curve()
True

In summary: yes, those are all the points, as the documentation claims.

The answer given would be correct in an ideal world. Unfortunately there are (1) bugs in the implementation, and also, sadly (2) bugs in the description of the algorithm in Henri COhen's book, because he takes some formulas from Smart's book, which Smart gets from the monograph of Sinou David, but he (Smart) does so incorrectly. (It's a question of which order you put the generating periods: is is w1/w2 or w2/w1 which is in the fundamental region. HC knows about this (I informed him) but I don't think that there is yet a correction on his web page (which has 20 pages of errata for the two volumes).

I am preparing a better implementation -- have been doing so for a few years now -- but currently you can not assume that the list of integral points output by Sage for elliptic curves over Q is complete, even if you have the full Mordell-Weil group. When I compute integral pints for the curve in the LMFDB I do so using both Sage and Magma and take the union. It is some time since I saw any integral points found by Sage not found by Magma, but in fairness I should say that while I was testing the first implementation of integral points in Sage (in 2008) that happened a lot, and as a result the Magma code was completely rewritten by Steve Donnelly, using several tricks he thought up but which have never been published.