#
Starred repositories
[NeurIPS 2024 Spotlight] Implementation of the paper "3D Gaussian Splatting as Markov Chain Monte Carlo"
The Replica Dataset v1 as published in https://arxiv.org/abs/1906.05797 .
Collections of useful mathematical statements in lean.
Learn Qiskit with Qiskit Textbook
Proof artifact co-training for Lean
The Lean Theorem Proving Environment
Template for blueprint-driven formalization projects in Lean.
A PyTorch implementation of the paper "EDGS: Eliminating Densification for Efficient Convergence of 3DGS"
Replay the `Environment` for a given Lean module, ensuring that all declarations are accepted by the kernel.
A Lean tactic that invokes the Kimina Prover Preview model to offer proof suggestions.
Repository for formalization of the Polynomial Freiman Ruzsa conjecture (and related results)
[CVPR 2024 Highlight] Scaffold-GS: Structured 3D Gaussians for View-Adaptive Rendering
source code for our work "CompGS: Efficient 3D Scene Representation via Compressed Gaussian Splatting"
Technical report of Kimina-Prover Preview.
Official PyTorch implementation of One-Minute Video Generation with Test-Time Training
Suggested conventions and examples for Lean formalization of IMO problem statements
cvc5 is an open-source automatic theorem prover for Satisfiability Modulo Theories (SMT) problems.
LeanEuclid is a benchmark for autoformalization in the domain of Euclidean geometry, targeting the proof assistant Lean.
Unified Efficient Fine-Tuning of 100+ LLMs & VLMs (ACL 2024)
Minimal reproduction of DeepSeek R1-Zero