3 ms·

Yes, once you formalize (in computer code) a bit of mathematics you can run it, but i'm pointing out that you don't need to formalize (the correctness of) a pro

• nmrm2 11y ago
  You also don't have to prove a theorem in order to use it. To give an elementary example, you can conjecture that a given mapping is something-morphism between two groups and use that morphism to carry out a proof about one group in terms of a known result about the other group. In fact, "conjecture lemma; verify main result is true using the conjectured lemma; go back an prove lemma" is a bog standard problem solving technique in Mathematics... edit: Oh, I see what you mean is bit more nuanced than I understood at first. But this is still true -- often you can probably check that the mapping you've written down is a something-morphism locally, for the elements you're working with atm. I'm stretching the example now, but you get my point? I imagine this is probably not unheard of in research-grade mathematics -- e.g. we don't have a general proof for "really cool conjecture" so we check it in special cases whereever we think it might be useful to have... idk.