Non omnes formulae significant quantitatem, et infiniti modi calculandi excogitari possunt. (Leibniz)
Copyright © 2023 -2026 Clarence Lewis Protin. All Rights Reserved
Investigations into the Idris2 proof assistant and some formalizations
Is there a proof assistant which combines the best aspects of Coq/Rocq and Agda? We would like the construction of proof-terms be done in a ...
-
No, a mathematical model of consciousness is not possible. First we must distinguish between the natural consciousness of Dasein studied acc...
-
It is difficult to evaluate the quality of mathematical work or the particular destiny of mathematics in the 20th century. We have already g...
-
https://www.researchgate.net/publication/385750025_Pierre_Cartier_A_Visionary_Mathematician