jesse-michael-han

I am a PhD student at the University of Pittsburgh, under the supervision of Tom Hales.

University of PittsburghPittsburgh

Pinned Repositories

colada-parser
A parser for Colada, a controlled natural language for the calculus of inductive constructions
Language:Haskell1 2 00
flypitch
A formal proof of the independence of the continuum hypothesis
Language:Lean0 1 00
lean
Lean Theorem Prover
Language:C++1 1 00
lean-coffee-can
Language:Lean1 2 00
lean-gptf
Interactive neural theorem proving in Lean
Language:Lean118 7 56
lean-parser-combinators
Monadic parser combinators, in Lean
Language:Lean4 2 00
lean-step-public
Proof artifact co-training for Lean
Language:Lean42 5 510
lean-tpe-public
The Lean Theorem Proving Environment
Language:Lean13 4 34
neuro-cadical
CaDiCaL + neural glue variable predictions
Language:Python9 4 02
neurocuber-public
Learning cubing heuristics for SAT from DRAT proofs
Language:Python5 2 00

jesse-michael-han's Repositories

jesse-michael-han/lean-gptf
Interactive neural theorem proving in Lean
Language:Lean118 7 56
jesse-michael-han/lean-step-public
Proof artifact co-training for Lean
Language:Lean42 5 510
jesse-michael-han/lean-tpe-public
The Lean Theorem Proving Environment
Language:Lean13 4 34
jesse-michael-han/neuro-cadical
CaDiCaL + neural glue variable predictions
Language:Python9 4 02
jesse-michael-han/neurocuber-public
Learning cubing heuristics for SAT from DRAT proofs
Language:Python5 2 00
jesse-michael-han/lean-parser-combinators
Monadic parser combinators, in Lean
Language:Lean4 2 00
jesse-michael-han/colada-parser
A parser for Colada, a controlled natural language for the calculus of inductive constructions
Language:Haskell1 2 00
jesse-michael-han/lean
Lean Theorem Prover
Language:C++1 1 00
jesse-michael-han/lean-coffee-can
Language:Lean1 2 00
jesse-michael-han/lean-demo
Language:Lean1 2 0
jesse-michael-han/flypitch
A formal proof of the independence of the continuum hypothesis
Language:Lean0 1 00
jesse-michael-han/arxivDownload
Language:Jupyter Notebook1 0
jesse-michael-han/cadical
Language:C++2 1
jesse-michael-han/doc-gen4
Document Generator for Lean 4
Language:Lean0 0
jesse-michael-han/drat-trim
The DRAT-trim proof checker
Language:C1 0
jesse-michael-han/flax
Flax is a neural network ecosystem for JAX that is designed for flexibility.
Language:Python1 0
jesse-michael-han/gptapiexperiment
Language:JavaScript0 0
jesse-michael-han/hanoi-lean-2019
Are you ready for Lean in Hanoi?
Language:Lean3 01
jesse-michael-han/lean-homotopy-theory
A development of homotopy theory in the Lean formal theorem prover.
Language:Lean1 0
jesse-michael-han/lean-sensitivity
A formalization of Huang's degree theorem
Language:Lean1 0
jesse-michael-han/legal-hackathon
Language:Python0 0
jesse-michael-han/mathlib
Lean mathematical components library
Language:Lean1 0
jesse-michael-han/mcmaster-thesis
MSc thesis
Language:TeX1 0
jesse-michael-han/mkplot
A Python script to create cactus and scatter plots based on matplotlib
Language:Python1 0
jesse-michael-han/open-wbo
Open-WBO: state-of-the-art MaxSAT and Pseudo-Boolean solver
Language:C++1 0
jesse-michael-han/oracle
Haskell prototype of the Search Transformer and Universal Oracle
Language:Haskell1 0
jesse-michael-han/ray
A fast and simple framework for building and running distributed applications. Ray is packaged with RLlib, a scalable reinforcement learning library, and Tune, a scalable hyperparameter tuning library.
Language:Python2 0
jesse-michael-han/smol_dev
Language:Python0 0
jesse-michael-han/theories-interpretations-pretoposes
Brief primer on first-order categorical logic
Language:TeX1 0
jesse-michael-han/yasnippet-lean
Language:Emacs Lisp1 0