This is a formalisation in Lean of the solution to Question 8 on the 2006 STEP 3 paper, which can be found here.
step3.lean is the solution which just uses the rules given in the question.
polynomial_derivations.lean builds up polynomial derivations, proving the structure theorem and also establishing an equivalence between polynomials and polynomial derivations.
step_3_derivations.lean is the solution to the problem which uses the polynomial derivations built up in the previous file.
Thanks to Kevin Buzzard for helping me do this.