From Newsgroup: comp.lang.prolog

Hi,

Remember DC Proof:

""DC Proof and Metamath provide very different approaches and
philosophies. DC Proof embeds first-order logic in its engine (program),
so that what the user sees corresponds to a more high-level view of the
proof, similar to what might be found in a math book or math course. DC
Proof is probably a better tool for learning about proofs in the way
that mathematicians usually do them."
--Norman Megill, creator of Metamath, sci.math, January 2006

DC Proof 2.0 - Testimonials 2013
http://www.dcproof.com/testimonials.htm

It was a free logic based fitch style proof construction
tool, unfortunately not open source. It could do some amazing
things. But for example I suspected it to be subject to

AmateurGate: DC Proof is subject to Grelling's antinomy https://groups.google.com/g/sci.logic/c/TaIENB54MNQ/m/0W9jjd-zAQAJ

Grelling's antinomy. But the ultimately battle ground was
a function space ontology with some useful extensionality.
In doubt Dan Christensen often refered to Terrence Tao,

as an authority of his modelling. But back in August 2023
there was only a verbal textbased reference for Analysis I.
This seems to have changed since May 2026:

A Lean companion to “Analysis I” https://terrytao.wordpress.com/2025/05/31/a-lean-companion-to-analysis-i/

Lean formalization of Analysis I
https://github.com/teorth/analysis

Now there is at least one official formal interpretation of
what Terrence Tao could have meant.

Bye
--- Synchronet 3.22a-Linux NewsLink 1.2