√2は単に x^2-2=0 の根であるということを意味する記号として扱える。
実際、数学の証明を書く場合にも、その正確な値を書くことなんてしないし、
証明に使う性質は、「x^2-2=0 の根である」という代数的性質から全て導かれる。

まあ、実際、代数学の証明の幾つかは既にコンピュータに載せられているものもあるし
人間が既にやった数学的証明は、コンピュータに載せることは可能。

ただし、コンピュータが人間の解いてない数学の定理を証明するような
自動証明ができるかどうかとなると話は別だが。