[randallholmes]

The problem I express relates to the issues people mention about libraries: if a defined concept is used, one has to be sure the definition is correct (i.e., that the right thing has been proved).

Wilshaw's formalization is not vulnerable to this objection, though libraries were used. What is proved is that a certain defined concept satisfies a certain suite of formulas of first order logic. If there is a predicate satisfying that suite of formulas, NF is consistent.

[randallholmes]

and it very much IS an essential part of my confidence in this proof that conversations between me and Sky Wilshaw reveal that she understands my argument [and was able to point out errors and omissions in paper versions!]

human interaction helps create confidence. But the software is extremely reliable: a philosophical challenge based on bugs in theorem proving software just is not going to hold water.

[pvg]

There's a (small, grey) link that reads 'edit' among the links at the top of each comment you can use if you want to change or add something to a comment you've already written, if you prefer that to replying to yourself.

[randallholmes]

I tried using it, and I could edit, but the update button did nothing; the edit never got posted. So I'll stick with little multiple replies for now.

[pvg]

The edit happens inline, immediately when you hit update - it won’t take you back to the thread but the comment is updated right above the input field (and in thread). It’s not terribly important either way.

[Smaug123]

I am sure you know this, but for the audience: the danger can be mitigated somewhat with a "test suite" of theorems and examples about the definitions. These examples can be very simple ("this particular object, with this particular operation, is a group; this other object is not") or much more sweeping and general (e.g. fundamental theorems like "all objects with this property are isomorphic" or "all objects with this property embed canonically in this other construction"). It doesn't prove that your definitions are correctly capturing what your natural-language proof talks about, but it can help you be more confident.