Important Questions

Who are you?

Wolf Honoré(on-a-RAY)

Where are you?

GitHub, USA Northeast, Email

What do you do?

Develop tools for formal verification of blockchain and smart contract code at CertiK. Basically, making it easier to either find bugs or prove they don't exist.

What did you used to do?

Curriculum Vitae
Computer Science BA and Applied Math BS from the University of Rochester in 2016, Computer Science PhD (and MS, MPhil) from Yale University in 2022. Some internships at SwRI doing things with visualizing map data, an internship at SiFive formally verifying a cache coherence protocol.

What do you like?

Programming/electronics projects, music, photography, running, cats.

Quick, can you prove √2 is irrational?

From Coq Require Import ssrbool ssreflect Lia QArith.

Lemma Qred_int x : Qred (x # 1) = x # 1.
Proof. by case: x => //; case. Qed.

Lemma Qmult_den p q r :
  p # q == r <-> p # 1 == (Z.pos q # 1) * r.
Proof.
  set den := inject_Z (Z.pos q).
  by rewrite !Qmake_Qdiv -[_ == r](Qmult_inj_l _ _ den)
             ?Qmult_div_r -?Qmake_Qdiv.
Qed.

Lemma even_sqr_even p : Z.even (p * p) -> Z.even p.
Proof. by rewrite Z.even_mul; case: orP => //; case. Qed.

Theorem sqrt2_irrational p q :
  Z.gcd p (Z.pos q) = 1%Z -> ~((p # q)^2 == 2 # 1).
Proof.
  set q' := Z.pos q; move=> Hred.
  rewrite Qmult_den -Qred_eq_iff ?Qred_int.
  case; rewrite ?Pos2Z.inj_mul; move=> Heq; move: Hred.
  have /Z.even_spec[k Hk]: Z.even p by apply even_sqr_even;
    rewrite Heq Z.even_mul orb_true_r.
  have Heq': (q' * q' = k * k * 2)%Z by lia.
  have /Z.even_spec[? Hq]: Z.even q' by apply even_sqr_even;
    rewrite Heq' Z.even_mul orb_true_r.
  rewrite Hk Hq Z.gcd_mul_mono_l; lia.
Qed.