alreadydone
PhD in Math, working on Lean's mathlib4 and formalization of FLT. Interested in autoformalization and AI for mathematics.
Heidelberg / Shenzhen
Pinned Repositories
2048-AI
A simple AI for 2048
AlphaMath
Deep reinforcement learning of mathematics in formal systems. Under construction, proposal available as pdf.
contents
GitHub issues as a blog with comment feature, place to publish and/or relay contents, and open discussion forum.
fusible
Exploration in fusible numbers
incredible
The Incredible Proof Machine
KataGo
GTP engine and self-play learning in Go
lz
Go engine with no human-provided knowledge, modeled after the AlphaGo Zero paper.
mathlib4
The math library of Lean 4
incredible
The Incredible Proof Machine
alreadydone's Repositories
alreadydone/lz
Go engine with no human-provided knowledge, modeled after the AlphaGo Zero paper.
alreadydone/formalising-mathematics
Material for Kevin Buzzard's 2021 TCC courrse on formalising mathematics.
alreadydone/fusible
Exploration in fusible numbers
alreadydone/mathlib
Lean mathematical components library
alreadydone/OthelloSearch
Shortest paths to reach specific configuration in the game of Othello/Reversi/黑白棋.
alreadydone/PhyloM
Tumor Phylogeny Topology Inference via Deep Learning
alreadydone/ai4math-papers
AI for Mathematics (AI4Math) paper list
alreadydone/alphafold
Open source code for AlphaFold.
alreadydone/AlphaGeometry
alreadydone/alreadydone.github.io
alreadydone/blog
Source for the community blog
alreadydone/discrete_fibrations
Here we compare the definitions of the category of presheaves as discrete fibrations and as functors into the universe
alreadydone/edax-reversi-AVX-v446mod2
alreadydone/elan
A Lean version manager
alreadydone/elliptic-curve
singular points & discriminant, etc.
alreadydone/FLT
Ongoing Lean formalisation of the proof of Fermat's Last Theorem
alreadydone/lean
Lean Theorem Prover
alreadydone/lean-chat
alreadydone/lean4
Lean 4 programming language and theorem prover
alreadydone/llama
Inference code for LLaMA models
alreadydone/math-lm
alreadydone/mathlib-tools
Development tools for https://github.com/leanprover-community/mathlib
alreadydone/mathlib4
The math library of Lean 4
alreadydone/mathQ
Data and code for the paper "A Neural Network Solves, Explains, and Generates University Math Problems by Program Synthesis and Few-Shot Learning at Human Level" by Drori et al., 2022.
alreadydone/MITQ
alreadydone/MU5735-ADSB-Reveal
alreadydone/ray
Formalizing results about the Mandelbrot set in Lean
alreadydone/sgx-genome-variants-search
alreadydone/shanghai-lockdown-covid-19
Coronavirus (COVID-19) statistics data in Shanghai lockdown. 封控期间上海疫情数据，包括病例数、死亡数、确诊数、无症状数和疫情地址等。
alreadydone/stacks-project
Repository for the Stacks Project