What can be learned from failed proofs of non-theorems?

This paper reports an investigation into the link between failed proofs and non-theorems. It seeks to answer the question of whether anything more can be learned from a failed proof attempt than can be discovered from a counter-example. We suggest that the branch of the proof in which failure occurs can be mapped back to the segments of code that are the culprit, helping to locate the error. This process of tracing provides finer grained isolation of the offending code fragments than is possible from the inspection of counter-examples. We also discuss ideas for how such a process could be automated.

A Mixed Discontinuous Galerkin Method for Incompressible Magnetohydrodynamics

We introduce and analyze a discontinuous Galerkin method for the numerical discretization of a stationary incompressible magnetohydrodynamics model problem. The fluid unknowns are discretized with inf-sup stable discontinuous P^3_{k}-P_{k-1} elements whereas the magnetic part of the equations is approximated by discontinuous P^3_{k}-P_{k+1} elements. We carry out a complete a-priori error analysis and prove that the energy norm error is convergent of order O(h^k) in the mesh size h. We also show that the method is able to correctly capture and resolve the strongest magnetic singularities in non-convex polyhedral domains. These results are verified in a series of numerical experiments.