Important Questions

Who are you?

Wolf Honoré(on-a-RAY)

Where are you?

GitHub, USA Northeast, Email

What do you do?

Formally verify AWS authorization and authentication as part of Amazon's Automated Reasoning group.

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. Developed tools for formal verification of smart contracts at CertiK.

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.