I think the answer that has the most votes, while good in and of itself, does not do justice to your question.
In some ways, the cleavage between "mathematical" statements as you call them, and empirical relates to, as another poster noted, the distinction between analytic (truth-functionally true) and contingent (not truth-functionally true). I'm using these roughly as the logical positivists did, and as they are defined in first-order logic.
A logical theorem, e.g. modus ponens, is analytic/truth-functionally true. As is a proof of Fermat's Theorem, and mathematical proof generally. Your characterization of "mathematical" based on the example you gave, corresponds to what in various ways has been called analytic or necessary propositions. These can uncouple depending on further assumptions. (Kant's definition of analytic would not apply here as it's limited to definitions only).
So to answer your question more robustly: the distinguishing criterion is a theory of deductive proof. Axiomatic systems are systems where given a few primitive assumptions (which themselves require no proof), all further statements, are formally deducible from them. Most accounts of proof, at least orthodox ones, are deductive in this way. This includes mathematical proof.
So this brings us to your last point:
Consider also the statement “Algorithm A will do task X faster than
Algorithm Y”. It is not immediately clear whether this statement is
empirical or mathematical.
There's a proof that a set of statements are Turing computable called the Church-Turing Thesis. This is a formal proof that has the following empirical implications: if a physical computer meets the minimal threshold of a general computer (Turing completeness), then it will compute at least a subset of Turing computable algorithms.
In other words, Turing computability refers to all the logically possible algorithms. But all the logically possible algorithms cannot be realized empirically. Why? Some empirical laws like entropy limit how much energy can be converted to work, and the availability of energy for conversion to work more generally.
As regards the efficiency of algorithms, my understanding is that you can give formal proofs for the limiting behaviour of a function as it approaches infinity for example. These are purely mathematical/deductive ways that have implications for all empirically possible/instantiated algorithms. However, once you built-in any empirical assumptions into your algorithm, namely about the way the world is, that is no longer a proposition justified by definitions, axioms, and proof alone. Every instantiation of an algorithm is empirical by nature and subject to empirical limits. However, algorithms in the abstract can be stated as proofs.
Note on Quine: I think it's well noted that this distinction as I have characterized it can be attacked, but it's important to begin with it first and expound justifications for it since so much of logic, set theory, mathematics rest on formal deduction. Anything not arrived at through deduction alone, can be said to be empirical.