2 ms·
> Honestly I’m not sure how you simultaneously claim to be a PhD in formalisation and also not be aware of the existence of Isabelle/ZF, for example. I am awar
by andriy_koval 1mo ago
> Honestly I’m not sure how you simultaneously claim to be a PhD in formalisation and also not be aware of the existence of Isabelle/ZF, for example.
I am aware, also I am not sure why you wrote all of this. Your unknown to me "first course" claims to be some authority of formalization purity?
- Smaug123 1mo agoBecause you wrote: > what are exactly rules, which could be separate topic of research, this detail is skipped I am now confident you’re a troll, though, so I am going to bow out.
- andriy_koval 1mo agoI referred to specific definition in wikipedia. Your "first course notes" are irrelevant here, they can't be reviewed, they not proofread and unlikely can be considered as any reasonable quality if we are talking about real formalization of math.