Is there a mathematical difference between currying and partial application? I know the following example doesn't make what I am saying rigorous, but hopefully it clarifies to some extent what I mean.

For various computer implementations, dividing by 2 and multiplying by 0.5 require a different number of CPU cycles, even though the two operations are mathematically equivalent. (The first is performing the inverse operation of multiplication with the number 2, which is defined to be multiplication by the multiplicative inverse of 2 which is $\frac{1}{2}$ or 0.5 in decimal.)

Google "practical difference between currying and partial application" and at least the entire first page of results explains some of my skepticism about whether there is a mathematical difference between currying and partial application -- none of the results treat the subject mathematically, i.e. by defining them in terms of Hom functors, and instead discuss how currying and partial application are implemented differently in most functional programming languages.
(In a nod to other websites in the StackExchange network, I will post the results from them:
https://stackoverflow.com/questions/218025/what-is-the-difference-between-currying-and-partial-application
https://softwareengineering.stackexchange.com/questions/290131/what-is-the-difference-between-currying-and-partial-function-application-in-prac)
Notice that in both of the examples given above, they fail to explain any mathematical difference -- instead the difference is explained with examples of lines of code.
While in practice, as in the case when differentiating dividng by 2 and multiplying by 0.5, there is a difference in implementation, it does not seem to amount to a theoretical difference.
 A: Currying and partial application are two different concepts, which impose different requirements on the category $\mathcal{C}$. Currying is a strictly stronger concept: one can express partial application using currying, but partial application is not sufficient for currying.
Currying (in cartesian closed category $\mathcal{C}\,$)
In order to talk about currying, the category has to be cartesian closed. In particular, it has to have exponential objects $Y^X$ for any two objects $X$ and $Y$. Currying is then one direction of the adjunction
$$ \mathcal{C}(X \times Y, Z) \cong \mathcal{C}(X, Z^Y)\qquad,$$
meaning that whenever we are given an $f: X \times Y \to Z$, we can obtain the curried version $\lambda f: X \to Z^Y$.
Partial application (in category with finite products)
For partial application, one needs only a category with all finite products (not necessarily cartesian closed). Since there is a terminal object $\mathbb{T}$ (nullary product), it makes sense to talk about elements of objects $X$: an element of $X$ can be defined as a morphism from $\mathbb{T} \to X$. Given an $f: X \times Y \to Z$, we can partially apply $f$ to $x$ as follows:
  $$ f \circ \langle x \circ \dagger_Y, Id_Y \rangle $$
where $\dagger_Y$ is the terminal morphism $Y \to \mathbb{T}$, the little circle $\circ$ denotes morphism composition, and $\langle - , - \rangle$ denotes the mediating morphism for products. If we now take any element of $Y$, that is, a morphism $y: \mathbb{T} \to Y$, and feed it to the above construction, we obtain:
$$ f \circ \langle x \circ \dagger_Y, Id_Y \rangle \circ y = f \circ \langle x \circ \dagger_Y \circ y, Id_Y \circ y \rangle = f \circ \langle x \circ Id_{\mathbb{T}}, y \rangle = f \circ \langle x, y \rangle \quad,$$
which is exactly what we would expect from a "partially applied function". Notice: we have built the morphism for "f partially applied to x" without using $\lambda$ or exponential objects. We don't need the full-blown cartesian closedness for that.
Expressing partial application through currying
Suppose that $\mathcal{C}$ is cartesian closed, let $f$, $x$, $y$ as above.
We can curry $f$ and apply it to $x$:
   $$ \lambda f \circ x \quad ,$$
obtaining an element of $Z^Y$. In order to be able to postcompose it with $y$, we have to "unpack" the element of $Z^Y$ using the evaluation morphism $\epsilon: Z^Y \times Y \to Z$. Thus, the morphism that represents "f partially applied to x" is:
  $$ \epsilon \circ \langle \lambda f \circ x \circ \dagger_Y, Id_Y\rangle \,.$$
Using the universal property of $\lambda f$ and $\epsilon$ (the commuting triangle that one sees in the definition of exponential objects), we can calculate:
  $$ \epsilon \circ \langle \lambda f \circ x \circ \dagger_Y, Id_Y\rangle = 
     \epsilon \circ (\lambda f \times Id_Y) \circ \langle x \circ \dagger_Y, Id_Y \rangle = f \circ \langle x \circ \dagger_Y, Id_Y \rangle \,,$$
thus our notion of "partial application" defined directly coincides with the notion of "partial application" defined through currying. That means, it does not matter which defintion we take in cartesian closed categories. 
When does the difference matter ...
...in programming:
Since categories built into functional programming languages (like $\mathrm{Hask}$) are cartesian closed, it does not really matter when creating simple functional programs.
However, as soon as we start to implement other categories inside our functional programming languages, the difference between "currying" and "partial application" begins to influence our design decisions. In general, it should be much easier to provide only finite products (which allow us to implement partial application), without providing currying. If we use those categories to represent certain computations, providing exponential objects and currying makes the framework more expressive, but we usually lose the possibility to inspect the structure of the computation before evaluating it. This is somewhat similar to trade-off between monads and applicatives: monads are more powerful, but applicatives have a more rigid structure, which can be analysed and optimized much better.
...in mathematics:
There are countless examples when one wants to have partial application, but does not want to think about whether the category one is working in is cartesian closed. 
For example, in classical multivariate calculus, we look at smooth functions from $\mathbb{R}^n \to \mathbb{R}^m$, and often want to fix some of the variables, and compute partial derivatives. It is crucial that we do this using only the product structure and partial application, but no currying: if we would take a multivariate function $f: \mathbb{R}^2 \to \mathbb{R}$, and then curry it, we would obtain something like a function from $\mathbb{R}$ to the function space $\mathbb{R} \to \mathbb{R}$, and would thereby fall out of the realm of classical multivariate calculus, and land in the realm of functional analysis.
Same with topology: we often want to take some continuous function that depends on multiple variables (some homotopy or something), then fix some of the variables, and argue that the partially applied function is still continuous, and work with that. In basic topology, we do not want to spend lot of time on defining topologies on function spaces, and trying to make the category of topological spaces cartesian closed. We don't have to, because partial application works without currying.
Code examples
The fact that we do not need currying in order to implement partial application can be illustrated in any functional programming language.
The following code snippets show how to implement partialApplication in terms of compose, identity and product, without using lambdas.
Scala (with detailed comments):
// suppose that we are given only identity morphisms,
// composition, terminal morphisms, and products of morphisms 
// (mediating morphism for product object)
// [BEGIN: assume that we can treat Scala functions as a "category with products"]
def identity[X]: X => X = x => x
def compose[X,Y,Z](g: Y => Z, f: X => Y): X => Z = x => g(f(x))
def terminal[X]: X => Unit = x => ()
def product[X, Y, Z](fst: X => Y, snd: X => Z): X => (Y, Z) = x => (fst(x), snd(x))
def constant[X](x: X): Unit => X = u => x
// [END: assume]

// We do not need any lambdas in order to express 
// partial application!

// non-strict version (x is a morphism that takes unit)
def partialApplication[X, Y, Z](f: ((X, Y)) => Z, x: Unit => X): Y => Z = 
  compose(f, product(compose(x, terminal[Y]), identity[Y]))

// strict version, uses const to transform `x` into constant function
def partialApplication[X, Y, Z](f: ((X, Y)) => Z, x: X): Y => Z = 
  compose(f, product(compose(constant(x), terminal[Y]), identity[Y]))

// example
val f: ((Int, Double)) => Double = {
  case (n, t) => math.cos(2 * math.Pi * t)
}
val f42 = partialApplication(f, 42)
println(f42(1.0))

The same in Haskell (same comments as in Scala apply):
identity :: a -> a
identity x = x
compose :: (y -> z) -> (x -> y) -> (x -> z)
compose g f = g . f
prod :: (x -> y) -> (x -> z) -> (x -> (y, z))
prod a b = \x -> (a x, b x)
terminal :: a -> ()
terminal x = ()
constant :: x -> (() -> x)
constant x = \u -> x

partialApplication :: ((x, y) -> z) -> (() -> x) -> (y -> z)
partialApplication f x = 
  compose f (prod (compose x terminal) identity)

A: I see that this question has already some good answer. Nonetheless allow me to give a personal perspective on the matter.
The definition of currying and partial application are the following:


*

*currying is an operation that takes a function of two (or maybe more argument) and return a function-valued function

*partial application is an operation that takes a function and a value and return the function with one argument bound to a given constant


these definition pretty much correspond to the ones given in wikipedia (follow the link).
In particular if you take a close look at this you can see that formally the operations currying and partial evaluation have the following types
$$\text{curry} \colon [X \times Y, Z] \longrightarrow [X,[Y,Z]]$$
$$\text{partEval}_X \colon [X \times Y,Z] \times X \to [Y,Z]$$
$$\text{partEval}_Y \colon [X \times Y,Z] \times Y \to [X,Z]$$
In particular partial evaluation is exactly what the name says: it is an evaluation that does not evaluate all the arguments of the function.
Hope this helps.
A: Not really if you are considering pure category theory (as the tag suggests):
$$\operatorname{Hom}(X \times Y, Z) \cong \operatorname{Hom}(X, \operatorname{Hom}(Y,Z)).$$
As usual when you have a canonical natural isomorphism, in most context you can replace one object with the other without changing anything.
The notions of "returning" and "evaluating" and so on don't really make sense from this point of view -- all this terminology comes from a world when functions have so-called "side effects". How would you model this mathematically?
add = function(x) {
    print("Hello there!");
    return function(y) {
        return x + y;
    }
}

Here there is a very clear difference between first applying the function to some given x and considering the result, and considering something like f(y) = add(2,y). In other words, we have a function of type Int -> (Int -> Int) that does not come from partial evaluation of a function Int * Int -> Int.
But we're way outside the world of mathematics now. As soon as you're explaining something in terms of "applying" or "evaluating" and then the function "returns" something and so on, you've veered away from category theory and into something else. In mathematics it doesn't matter if I "compute" $f(x)$ now or tomorrow or 100 years from now.
A: As far as I can tell, the only real difference that is ever noted is that partial application combines two steps into one: (1) first it curries a function $f$ and then (2) evaluates the resulting curried function $\tilde{f}$ with a given value.
But then, at least in my unimportant opinion, that shouldn't be called "partial application", since one would expect such a term to be agnostic with respect to what the given value will be in advance. That should instead be "partial application at a given value". But if we partially apply a function of two arguments, for example, but don't specify in advance at what value the curried function will be evaluated, then isn't that just currying? I.e., if given $f(x,y)$ we return $\tilde{f}(z): f(x,y) \mapsto f(z,y)$, then aren't we returning a function with one argument which returns a function of one argument, rather than a function of one input argument which returns a real number, say like $f(2,y)$? 
From this viewpoint it doesn't seem like currying and partial application are different at all, since mathematically if you "fix" a value without specifying what the exact value will be, you are just returning the curried function. In other words, I would describe currying as "fixing one of the  $n$ arguments of $f$ to return a new function $\tilde{f}$ which takes one argument as input and returns a function of $n-1$ arguments as output, and partial application as currying and then evaluating the curried function, e.g. $\tilde{f}(2)=f(2,y)$.
EDIT: According to Wikipedia, this is exactly the only difference.
See: https://en.wikipedia.org/wiki/Currying#Contrast_with_partial_function_application

Partial application can bee seen as evaluating a curried function at a fixed point

Therefore I am just going to post this as community wiki, so it won't affect my reputation, but will hopefully show up in Google search results for anyone in the future who ends up asking a similar question.
