Next thing would be trimming the DejaVuSans font to keep only the 10 or so mathematical symbols I need (to reduce size).
I've tried to do so online with the font generator here:
http://www.fontsquirrel.com/tools/webfont-generator
But so far, it doesn't trim: the output is as big as the input, whatever 'expert' settings I choose.