Pinned Repositories
Coq-HoTT
A Coq library for Homotopy Type Theory
coq-scripts
Various useful scripts for dealing with Coq files
coq-tactics
Collection of tactics I've found useful in Coq
coq-tools
Some scripts to help construct small reproducing examples of bugs, implement [Proof using], etc.
guarantees-based-mechanistic-interpretability
lob
Two attempts at formalizing Löb's Theorem, (one based on http://lesswrong.com/lw/t6/the_cartoon_guide_to_l%C3%B6bs_theorem/)
lob-paper
A write-up of https://github.com/JasonGross/lob
tikzplotlib
:bar_chart: Save matplotlib figures as TikZ/PGFplots for smooth integration into LaTeX.
unsong_scraper
Unsong for kindle, based on https://github.com/rhelsing/worm_scraper
fiat-crypto
Cryptographic Primitive Code Generation by Fiat
JasonGross's Repositories
JasonGross/coq-tools
Some scripts to help construct small reproducing examples of bugs, implement [Proof using], etc.
JasonGross/tikzplotlib
:bar_chart: Save matplotlib figures as TikZ/PGFplots for smooth integration into LaTeX.
JasonGross/guarantees-based-mechanistic-interpretability
JasonGross/coq-scripts
Various useful scripts for dealing with Coq files
JasonGross/neural-net-coq-interp
Some experiments with doing NN interpretability in Coq
JasonGross/guarantees-based-mechanistic-interpretability-with-data
JasonGross/coq
Coq is a formal proof management system. It provides a formal language to write mathematical definitions, executable algorithms and theorems together with an environment for semi-interactive development of machine-checked proofs.
JasonGross/JasonGross.github.io
My personal website
JasonGross/wysiwygpicture
A WIP project on turning Adobe Reader into an interactive editor for the the `picture` environment in LaTeX, spun off from https://tex.stackexchange.com/questions/719482/turning-adobe-reader-into-an-interactive-picture-editor
JasonGross/bedrock2
Towards a low-level systems programming language with a verified compiler
JasonGross/bot
A (Coq Development Team) bot written in OCaml
JasonGross/CompCert
The CompCert formally-verified C compiler
JasonGross/delta
Delta assists you in minimizing "interesting" files subject to a test of their interestingness.
JasonGross/devinterp
Tools for studying developmental interpretability in neural networks.
JasonGross/fiat-crypto
Cryptographic Primitive Code Generation in Fiat
JasonGross/guarantees-based-mechanistic-interpretability-data
JasonGross/inspect_ai
Inspect: A framework for large language model evaluations
JasonGross/mathlib4
The math library of Lean 4
JasonGross/memocache
An overengineered solution to memoization and caching
JasonGross/metacoq
Reflection library for Coq
JasonGross/MultiDimensionalFeatures
Code for reproducing our paper "Not All Language Model Features Are Linear"
JasonGross/ocamlfind
The OCaml findlib library manager
JasonGross/openreview-exploration
Scripts for exploring openreview submissions
JasonGross/publications
A .bib file of my publications
JasonGross/readwise-export
An exporter for readwise data
JasonGross/resume
My resume and CV
JasonGross/scipy
SciPy library main repository
JasonGross/test
Testing repo for playing with things on GitHub
JasonGross/TransformerLens
A library for mechanistic interpretability of GPT-style language models
JasonGross/wasm_of_ocaml