[FOM] Defining Cargo Cult Science in Mathematics

[Sam Sanders]

Dear José,

>  I would like to propose that a candidate mathematical-like theory is CCS if it cannot be developed in a proof assistant. Otherwise, it is a genuine mathematical theory.

What about the following problem: choosing the right definitions is extremely important when doing constructive math, and even more so when formalising math
in proof assistants. For instance, Larry Paulson has formalised Godel’s incompleteness theorems in Isabelle using the notion of “hereditarily finite set”.  He used 
this particular notion because other notions did not (seem to) yield a formal proof (I am citing from memory about a talk he gave at TU Munich). IIRC, he even wrote 
(or rewrote?) a version of Sledgehammer to accommodate this notion.  

Are we therefore to conclude that this particular formulation (using hereditarily finite sets) of Godel’s incompleteness theorems is genuine and the others are not?

Moreover, what if different parts of math require different (but equivalent, say in ZFC) definitions to successfully obtain formal proofs?  

Finally, it seems your notion of “genuine vs CCS” includes some kind of implicit strict finitism (and temporal/physical dimension): for a given theorem to be implemented in a 
proof assistant, there have to be “good” definitions that result in a proof that can be run on a physical machine (in the here and now).  

The previous does present a nice  “incompleteness” challenge: find a natural theorem that cannot be implemented in proof assistants, 
in that any choice of definitions for that theorem results in infeasible computation at the level of implemented proofs.  

Best,

Sam