Finite Methods in Mathematical Practice

In the present contribution we look at the legacy of Hilbert’s programme in some re- cent developments in mathematics. Hilbert’s ideas have seen new life in generalised and relativised forms by the hands of proof theorists and have been a source of motivation for the so–called reverse mathematics programme initiated by H. Friedman and S. Simp- son. More recently Hilbert’s programme has inspired T. Coquand and H. Lombardi to undertake a new approach to constructive algebra in which strong emphasis is laid on the use of finite methods. The main aim is to eliminate the ideal objects and in so doing obtain more elementary and informative proofs. We survey some work in commutative algebra—mainly about and around the Zariski spectrum and the Krull dimension of a commutative ring—which witnesses the feasibility of such a revised Hilbert’s programme.