Leibniz was an independent inventor of the calculus (the other was Newton), which is of central importance to any attempt
to automate reasoning about the real world.
The branch of mathematics which this inaugurated is now called "analysis".
It is extensively used in science and engineering and is in that way the basis for most applications of mathematics to the
real world.

This work was however, controversial, from its inception, doubts being raise (for example by the Irish philosopher Berkeley)
about its coherence (mostly because of its use if

*infinitesimal* or infinitely small) quantities).
One of the major problems in realising Leibniz's dream is to make it possible to reason rigorously about this kind of mathematics.
This involved the rigourisation, arithmetisation and logicisation of analysis, the development of adequate logical systems
for this kind of mathematics, the invention of the digital computer and the implementation of software supporting formal reasoning
in the new logics, and by that means in arithmetic and analysis.