[pa7x1]

It's both. The axioms are invented, the corpus of theorems is discovered. As once the axioms are chosen the provable theorems are already fixed.

But the axioms are a choice, and we can pick different ones. The common choice of axioms is utilitarian, they lead to interesting math that helps us describe the universe.

[Mimmy]

I would agree the axioms are chosen, but what’s the connection between choosing something and inventing it?

Choosing to study molecular biology doesn’t mean cells are a human invention.

[mensetmanusman]

That the universe chose axioms is indeed the mystery.

[openquery]

Proving a theorem given a set of axioms is a search problem. Given a set of axioms you can apply rules of inference to generate the graph of all provable theorems. Proving a theorem is about finding a path from the axioms to the vertex which is your theorem.

But you can make the same case for axioms - that they are not invented but discovered through a process of search in the space of axioms.

[sweezyjeezy]

I'm not sure I see why the axioms were not also discovered though? Choice between irreducible assumptions does not seem to make them any more 'invented'.

[pa7x1]

Without entering into an endless debate about semantics and metaphysics I would simply say that if you want to use the word discovered for the axioms then you must acknowledge that the theorems are not the same kind of discovered.

[hurryer]

What about natural numbers?

I've read that Godel's result and diagonalization procedure shows that they exist (not invented).

[random3]

Are the theories beyond axiom fundamentally different if axioms are changed, though? And if not, aren't then axioms merely props or placeholders for invariants?

[sweezyjeezy]

Yes they are different - example: https://en.m.wikipedia.org/wiki/Parallel_postulate