Projects Related to Derivations

The goal in Derivations is to develop a rigorous acccount of undergraduate math concepts, following four fundamental principles:

1. No magic lemmas. Theorems should be broken down into steps that are motivated, that actually seem like a step towards the goal, before those steps are proved. e.g. don't prove Rolle's theorem until after you can explain what that has to do with Taylor polynomials.
2. No magic formulas. Before you even state the goal of a theorem or lemma, the individual operations and formulas should themselves have emerged naturally in the course of proving earlier theorems. e.g. don't even state Taylor's theorem as a goal until you can explain why Taylor polynomials are interesting and useful all on their own.
3. Respect common language. If academic language would allow a set to be both open and closed, or for continuous functions to have jumps, then academic language is wrong, not common language.
4. Emphasize computation and real-world inference. Differential and integral calculus are used by real people to infer real facts about the world every day; a rigorous account of mathematics should rigorously explain why that is possible, not just why some theorems follow from some arbitrary choice of axioms.

I have found derivations for a good deal of calculus, analysis, and linear algebra results that follow these principles, but I haven't found a good work flow that allows me to work with mathematical notation and hypertext easily. So far I have

• Derivations, where all the results I have worked out are listed, but most are not written up.
• A single Medium article explaining how to formalise continuity in the sense that most people think they mean - a function without big jumps or gaps in it.
• A Twitter thread explaining continuity informally, based on the Medium article.
• A roughly 20 page document deriving rotors and quaternions following the above principles, using the properties of determinants as prior theory.

I'd like some wiki software that can let me do some of these things properly, but even then it will still be a massive time-sink, all for math 'education' articles that most people don't understand anyway.

Plotting and Visualisation Software

Something that would go much further to 'emphasize computation' in this project would be plotting environments and algebraic systems that can demonstrate some of the intermediates in interactive ways, like plotting the errors and rates of convergence of different analytic solutions to calculus problems, or a sequence of plots of the LHS and RHS of each line in the process of solving an algebraic equation.

An early influence on my computable calculus work, but which I originally only did for game development purposes, was a custom bigint implementation of some transcendental functions. First I made the bigints, and big complex numbers, used that to implement an arbitrarily accurate (turn angle) arctan implementation, which I could then invert to get tan, or apply to small values to find a hand-rolled, arbitrarily accurate algorithm for calculating digits of pi. I was able to extend this approach to arcsin, sin, cos, log, and exponentials, all in binary and/or turn-angle units, and calculate euler's number, square roots, etc.

The real goal of these slow but accurate calculations though, was to provide a function that I could sample, to implement the Remez algorithm, and roll my own polynomial approximations of those functions. I didn't manage it in the C, but starting over in Rust did the trick, and I got my own polynomial approximations of a number of functions, which are now just waiting for a use case. The source code for both the C implementations and the Rust implementations can be at github.com/spiveeworks/fix-math.

In between the C and Rust implementations of these things, I wanted to make a plotting environment that would let me implement some of these things in a way that might be more literate, and easier to visualise, at the same time. I didn't get very far, but some projects can be found in different branches of this repository. Notably

• old_app where I first started plotting and bisecting polynomials,
• colour-rhombohedron where I plotted a hexagonal cross-section of the RGB cube, to visualise how the color wheel looked like when presented linearly like that,
• erlang-port where I made a crappy virtual machine for calculations that could be controlled via a higher level erlang interface. The hope was that I could use erlang instead of making a new language, but it quickly turned out that the 'erlangy' way to do what I was trying to do was to make a language anyway,
• midpoint-hull where I explored someone's stackoverflow question after QC shared his answer to it. It was fun but I may have ruined everyone else's fun, not sure.

The plotting is all done using the X11/wingdi setup I used in Settlement. I keep trying to move to other languages and graphical environments to do calculations or plotting in, but I keep coming back to C... Apart from the Remez Algorithm part, which instantly clicked in Rust. I guess I better just finish making Phosphate then.

In reality I shouldn't make any new plotting environments anymore, and should just work out whatever Marc Ten Bosch uses on his wonderful site.