Maxima

Maxima ist ein freies Computer-Algebrasystem (CAS), mit dem sich formale Mathematik betreiben lässt.

Das System wurde u.a. in Hugemann: Unfallrekonstruktion dazu genutzt, komplizierte Umformungen automatisch durchzuführen bzw. zu beweisen.

Besonders einfach ist es, die formale Identität zweier Ausdrücke f(x) und g(x) zu beweisen, weil dann in Maxima nur f(x) - g(x) zu berechnen ist, und das Ergebnis Null lauten sollte. Auf diese Weise wurden etwa sämtliche händischen Berechnungen von Pfeufer, H. zu seinem Buchbeitrag formal geprüft.

Auch im Colliseum wird an einigen Stellen Maxima-Code als Beweis für die Gültigkeit bestimmter Umformungen angegeben, so etwa unter Topokol.

Soweit man die Programmumgebung von Maxima nicht vollständig auf dem Rechner installieren möchte, kann man unter http://maxima.cesga.es/ online Maxima-Code ausführen. Das funktioniert auch auf dem Smartphone.