По Isabelle/HOL вообще либо научные статьи, либо официальная дока

Ни тебе стековерфлоу, нихуя

А прувер то крутой, можно такую хуйню делать:

theorem sqrt2_not_rational:
  "sqrt (real 2) ∉ ℚ"
proof
  let ?x = "sqrt (real 2)"
  assume "?x ∈ ℚ"
  then obtain m n :: nat where
    sqrt_rat: "¦?x¦ = real m / real n" and lowest_terms: "coprime m n"
    by (rule Rats_abs_nat_div_natE)
  hence "real (m^2) = ?x^2 * real (n^2)" by (auto simp add: power2_eq_square)
  hence eq: "m^2 = 2 * n^2" using of_nat_eq_iff power2_eq_square by fastforce
  hence "2 dvd m^2" by simp
  hence "2 dvd m" by simp
  have "2 dvd n" proof -
    from ‹2 dvd m› obtain k where "m = 2 * k" ..
    with eq have "2 * n^2 = 2^2 * k^2" by simp
    hence "2 dvd n^2" by simp
    thus "2 dvd n" by simp
  qed
  with ‹2 dvd m› have "2 dvd gcd m n" by (rule gcd_greatest)
  with lowest_terms have "2 dvd 1" by simp
  thus False using odd_one by blast
qed

И ты доказал, что корень из двух нерационален

Тебе заняться нехуй ?

Да, а что?

Ладно, ничего

Ну типа мне нравится прогать, почему я не должен выходить за рамки комфорта (ЯП, который я хорошо знаю), и не решать челленжи, которые сам себе ставлю?

Все ок. Я не наезжаю

Спасибо

мужик, ты вроде боролся с файлами которые отправлял через тг бот, ты не натыкался на ограничение в 50 мб ?

Да, я на мтпрото пишу

Там ограничение, как у юзеров, 2 гига

это что то типа клиент-бот ?

нагуглил

Да