You have to keep in mind that when checking for an identity, Sage returns True
if it has been capable to prove the identity and False
if either (i) Sage has been capable to disprove it or (ii) Sage has not been capable to prove or disprove it. So, a False
output means either "false" or "unknown". For instance, on your example, we have
sage: bool(log(a / b) == log(a) - log(b))
False
sage: bool(log(a / b) != log(a) - log(b))
False
These two results seem contradictory, but here the two False
actually mean "unknown". This state of affairs is due to bool
implementing a bivalent logic, not a ternary one (which would have permit Unknown
as a possible output).
As @Emmanuel_Charpentier explains in his answer, you have to help Sage by invoking log_expand
:
sage: stmt = log(a / b) == log(a) - log(b)
sage: bool(stmt.log_expand())
True