Commits

Branch selector

master

User selector

All users

All time

Commit history

Commits on May 14, 2026

• Add equiangularity and extended top level statement

  Show description for 30e3439
  evfinkn

  committed
  30e3439View commit details

  Copy full SHA for 30e3439

  Browse repository at this point

Commits on Apr 28, 2026

• Substantially extended the probability theory library with new results,

  Show description for 3170739
  jrh13

  committed
  3170739View commit details

  Copy full SHA for 3170739

  Browse repository at this point

Commits on Apr 26, 2026

• Added more ring, group and permutation material

  Show description for d19bdec
  jrh13

  committed
  d19bdecView commit details

  Copy full SHA for d19bdec

  Browse repository at this point

Commits on Apr 21, 2026

• Use Num-specific comparison operators instead of generic OCaml ones on Num.num values

  Show description for 3bc3d27
  

  John Harrison

  authored and

  jrh13

  committed
  3bc3d27View commit details

  Copy full SHA for 3bc3d27

  Browse repository at this point

• Multivariate/vectors.ml: Use </ instead of < (#173)

  dnezam

  authored
  0a215a4View commit details

  Copy full SHA for 0a215a4

  Browse repository at this point

Commits on Apr 16, 2026

• Bump astral-sh/setup-uv from 4 to 7 (#172)

  Show description for c5d7fc1
  dependabot[bot]

  authored
  c5d7fc1View commit details

  Copy full SHA for c5d7fc1

  Browse repository at this point

• Bump actions/checkout from 2 to 6 (#171)

  Show description for 3be87b7
  dependabot[bot]

  authored
  3be87b7View commit details

  Copy full SHA for 3be87b7

  Browse repository at this point

• mcp: add CI, reduce dependabot false positives, and miscellaneous polishing (#169)

  Show description for 9fa0dff
  sgmenda

  authored
  9fa0dffView commit details

  Copy full SHA for 9fa0dff

  Browse repository at this point

Commits on Apr 15, 2026

• Add Tactician Light (#168)

  Show description for e8944de
  jargh

  authored
  e8944deView commit details

  Copy full SHA for e8944de

  Browse repository at this point

Commits on Apr 14, 2026

• Bump cryptography from 46.0.5 to 46.0.7 in /mcp (#165)

  Show description for 707941e
  dependabot[bot]

  authored
  707941eView commit details

  Copy full SHA for 707941e

  Browse repository at this point

Commits on Apr 13, 2026

• mcp: add proof recording and tactic replay (#167)

  Show description for 5be5325
  

  ckocaogullar

  and

  Ceren Kocaogullar

  authored
  5be5325View commit details

  Copy full SHA for 5be5325

  Browse repository at this point

• mcp/SKILL.md: add pitfalls and tactics from s2n-bignum GHASH proof work (#164)

  Show description for 9bfdc61
  

  nebeid

  and

  Kiro (Claude Opus 4.6)

  authored
  9bfdc61View commit details

  Copy full SHA for 9bfdc61

  Browse repository at this point

Commits on Apr 9, 2026

• mcp: structured JSON from eval/hol_load, output truncation, built-in timing (#163)

  Show description for 9359987
  sgmenda

  authored
  9359987View commit details

  Copy full SHA for 9359987

  Browse repository at this point

• Added a proof of Green's theorem in a fairly general form, autoformalized

  Show description for e99ed34
  jrh13

  committed
  e99ed34View commit details

  Copy full SHA for e99ed34

  Browse repository at this point

• Add word-level carryless multiplication operation word_pmul (#166)

  Show description for af5d20e
  jargh

  authored
  af5d20eView commit details

  Copy full SHA for af5d20e

  Browse repository at this point

Commits on Apr 7, 2026

• mcp: faster eval, new tools, fixed threading, fixed config finding (#162)

  Show description for 81f68c0
  sgmenda

  authored
  81f68c0View commit details

  Copy full SHA for 81f68c0

  Browse repository at this point

Commits on Apr 3, 2026

• make_checkpoint: run Gc.compact() before checkpointing (#161)

  Show description for 1eb5faf
  nebeid

  authored
  1eb5fafView commit details

  Copy full SHA for 1eb5faf

  Browse repository at this point

Commits on Apr 1, 2026

• Port the record feature from s2n-bignum (#156)

  aqjune-aws

  authored
  05dbdedView commit details

  Copy full SHA for 05dbded

  Browse repository at this point

• calc_num.ml: Use <=/ instead of <= (#155)

  Show description for a44a11c
  dnezam

  authored
  a44a11cView commit details

  Copy full SHA for a44a11c

  Browse repository at this point

• Add MCP server for HOL Light with structured proof tools (#157)

  Show description for 0821573
  sgmenda

  authored
  0821573View commit details

  Copy full SHA for 0821573

  Browse repository at this point

Commits on Mar 23, 2026

• Added the first version of a new probability theory library. This was

  Show description for 1c7690e
  jrh13

  committed
  1c7690eView commit details

  Copy full SHA for 1c7690e

  Browse repository at this point

Commits on Feb 28, 2026

• Added the Hahn-Mazurkiewicz, Alexandroff-Hausdorff and Menger

  Show description for 6df9b21
  jrh13

  committed
  6df9b21View commit details

  Copy full SHA for 6df9b21

  Browse repository at this point

• Restore compatibility with OCaml 4.06, Camlp5 7.10 (#154)

  Show description for 2264f31
  dnezam

  authored
  2264f31View commit details

  Copy full SHA for 2264f31

  Browse repository at this point

Commits on Feb 27, 2026

• Cleaning up metis (#152)

  Show description for d9a37c8
  dnezam

  authored
  d9a37c8View commit details

  Copy full SHA for d9a37c8

  Browse repository at this point

Commits on Feb 26, 2026

• Added material about algebraically closed fields, with a definition

  Show description for 955caa3
  jrh13

  committed
  955caa3View commit details

  Copy full SHA for 955caa3

  Browse repository at this point

Commits on Feb 22, 2026

• Added a formalization of the impossibility of cube dissection into

  Show description for c31563b
  jrh13

  committed
  c31563bView commit details

  Copy full SHA for c31563b

  Browse repository at this point

Commits on Feb 20, 2026

• Added some basic definitions and theorems about the Cantor space. The

  Show description for 3dbf53f
  jrh13

  committed
  3dbf53fView commit details

  Copy full SHA for 3dbf53f

  Browse repository at this point

• Added general metric space versions of well-chainedness, connectedness

  Show description for 2ce6c3e
  jrh13

  committed
  2ce6c3eView commit details

  Copy full SHA for 2ce6c3e

  Browse repository at this point

Commits on Feb 19, 2026

• Merge pull request #153 from jargh/master

  Show description for 9b73aef
  jrh13

  authored
  9b73aefView commit details

  Copy full SHA for 9b73aef

  Browse repository at this point

• Added a proof of Rabin's test for irreducibility of polynomials over

  Show description for 0c9e65f
  jargh

  committed
  0c9e65fView commit details

  Copy full SHA for 0c9e65f

  Browse repository at this point

Commits on Feb 16, 2026

• Added a definition of paracompactness to the core general topology

  Show description for 0a5e935
  jrh13

  committed
  0a5e935View commit details

  Copy full SHA for 0a5e935

  Browse repository at this point

• Merge pull request #151 from aqjune-aws/unify_refl

  Show description for c87954f
  jrh13

  authored
  c87954fView commit details

  Copy full SHA for c87954f

  Browse repository at this point

Commits on Jan 30, 2026

• Added a proof of Urysohn's metrization theorem and also a definition of set

  Show description for c845dd3
  jrh13

  committed
  c845dd3View commit details

  Copy full SHA for c845dd3

  Browse repository at this point

Commits on Jan 29, 2026

• Add UNIFY_REFL_TAC to unify metavariables in equality

  Show description for 4343a44
  aqjune-aws

  committed
  4343a44View commit details

  Copy full SHA for 4343a44

  Browse repository at this point

Commits on Jan 9, 2026

• Merge pull request #149 from aqjune-aws/fix-tactictrace

  Show description for e960dd0
  jrh13

  authored
  e960dd0View commit details

  Copy full SHA for e960dd0

  Browse repository at this point