-
University of Cambridge
- https://albertqjiang.github.io/
Highlights
- Pro
-
MMA Public
The official repository for the paper Multilingual Mathematical Autoformalization
-
ReProver Public
Forked from lean-dojo/ReProverRetrieval-Augmented Theorem Provers for Lean
Python MIT License UpdatedApr 5, 2024 -
alphageometry Public
Forked from google-deepmind/alphageometryPython Apache License 2.0 UpdatedFeb 8, 2024 -
LeanDojo Public
Forked from lean-dojo/LeanDojoTool for data extraction and interacting with Lean programmatically.
Python MIT License UpdatedJan 12, 2024 -
-
Portal-to-ISAbelle Public
https://albertqjiang.github.io/Portal-to-ISAbelle/
-
EasyLM Public
Forked from young-geng/EasyLMLarge language models (LLMs) made easy, EasyLM is a one stop solution for pre-training, finetuning, evaluating and serving LLMs in JAX/Flax.
-
-
lm-evaluation-harness Public
Forked from EleutherAI/lm-evaluation-harnessA framework for few-shot evaluation of autoregressive language models.
Python MIT License UpdatedApr 25, 2023 -
llama_on_mps Public
Forked from meta-llama/llamaInference code for LLaMA models
Python GNU General Public License v3.0 UpdatedApr 22, 2023 -
math_cc_net Public
Forked from zhangir-azerbayev/math_cc_netTools to download and cleanup Common Crawl data
Python MIT License UpdatedMar 28, 2023 -
submitit Public
Forked from facebookincubator/submititPython 3.6+ toolbox for submitting jobs to Slurm
Python MIT License UpdatedMar 23, 2023 -
scala-isabelle Public
Forked from dominique-unruh/scala-isabelleA Scala library for controlling/interacting with Isabelle
Scala MIT License UpdatedDec 29, 2022 -
-
INT Public
Official code for paper: INT: An Inequality Benchmark for Evaluating Generalization in Theorem Proving
-
miniF2F-1 Public
Forked from facebookresearch/miniF2FAn updated version of miniF2F with lots of fixes and informal statements / solutions.
Objective-C++ MIT License UpdatedNov 7, 2022 -
JAXSeq Public
Forked from Sea-Snell/JAXSeqTrain very large language models in Jax.
Python MIT License UpdatedOct 21, 2022 -
-
interactive_isabelle Public
Forked from TomaszOdrzygozdz/interactive_isabelleScala UpdatedJun 11, 2022 -
-
miniF2F_old Public
Forked from openai/miniF2FFormal to Formal Mathematics Benchmark
Isabelle UpdatedApr 12, 2022 -
-
mesh-transformer-jax Public
Forked from kingoflolz/mesh-transformer-jaxModel parallel transformers in JAX and Haiku
-
mathematics_dataset Public
Forked from google-deepmind/mathematics_datasetThis dataset code generates mathematical question and answer pairs, from a range of question types at roughly school-level difficulty.
Python Apache License 2.0 UpdatedJan 12, 2022 -
-
-
-
-
-