Regarding, footnote 1, two more relevant examples: First, Simon Colton has made a series of computer programs which can construct new definitions in number theory and make conjectures about them. See this paper. Second, the Robbins conjecture, a long time open problem in abstract algebra, was proven with some human intervention but mainly an automated theorem prover.
Regarding, footnote 1, two more relevant examples: First, Simon Colton has made a series of computer programs which can construct new definitions in number theory and make conjectures about them. See this paper. Second, the Robbins conjecture, a long time open problem in abstract algebra, was proven with some human intervention but mainly an automated theorem prover.