Skip to content


  • Arctic Code Vault Contributor



Popular repositories

  1. Metamath Zero specification language

    Rust 145 16

  2. mmj2 GUI Proof Assistant for the Metamath project

    Java 43 18

  3. LaTeX code for a paper on lean's type theory

    TeX 38 3

  4. Baezon's Redstone Simulator

    Java 8 2

  5. The Advent of Code programming puzzles in Lean

    Lean 7

  6. parser/viewer for olean files

    Rust 5 4

651 contributions in the last year

Jan Feb Mar Apr May Jun Jul Aug Sep Oct Nov Dec Jan Mon Wed Fri

Contribution activity

January 2021

Created 2 repositories

Created a pull request in leanprover-community/mathlib that received 5 comments

[Merged by Bors] - fix(tactic/rcases): fix rcases? goal alignment

This fixes a bug in which rcases? will not align the goals correctly in the same manner as rcases, leading to a situation where the hint produced by

+49 −6 5 comments
Opened 4 other pull requests in 3 repositories
Reviewed 4 pull requests in 2 repositories

Seeing something unexpected? Take a look at the GitHub profile guide.

You can’t perform that action at this time.