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.
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.