Jungforscher haben die Lösung für eines der Jahrhundertprobleme von Hilbert bestätigt, mit einem Mittel, von dem Hilbert damals nur träumen konnte: einer Software namens Isabelle.