Editing Constructive proof (section)

===Constructive proofs===

A ''constructive'' proof of the theorem that a power of an irrational number to an irrational exponent may be rational  gives an actual example, such as:
:<math>a = \sqrt{2}\, , \quad b = \log_2 9\, , \quad a^b = 3\, .</math>
The [[square root of 2]] is irrational, and 3 is rational. <math>\log_2 9</math> is also irrational: if it were equal to <math>m \over n</math>, then, by the properties of [[logarithms]], 9<sup>''n''</sup> would be equal to 2<sup>''m''</sup>, but the former is odd, and the latter is even.

A more substantial example is the [[graph minor theorem]]. A consequence of this theorem is that a [[graph (discrete mathematics)|graph]] can be drawn on the [[torus]] if, and only if, none of its [[minor (graph theory)|minors]] belong to a certain finite set of "[[forbidden minors]]". However, the proof of the existence of this finite set is not constructive, and the forbidden minors are not actually specified.<ref>{{Cite journal|last1=Fellows|first1=Michael R.|last2=Langston|first2=Michael A.|date=1988-06-01|title=Nonconstructive tools for proving polynomial-time decidability|url=http://www.mrfellows.net/papers/FL88_NonconstructiveTools.pdf|journal=Journal of the ACM|volume=35|issue=3|pages=727–739|doi=10.1145/44483.44491|s2cid=16587284}}</ref> They are still unknown.