wiio12

wiio12's Stars

• leanprover-community/repl

  A simple REPL for Lean 4, returning information about errors and sorries.

  Language:Lean8021

• marcusrossel/lean-egg

  A (WIP) equality saturation tactic for Lean based on egg.

  Language:Lean412

• srush/awesome-o1

  A bibliography and survey of the papers surrounding o1

  Language:TeX74133

• xqyww123/Isa-REPL

  Isabelle REPL

  Language:Standard ML10

• xqyww123/Isa-Proof-Shell

  A proof assistant adapter designed for machine learning

  10

• QwenLM/Qwen2.5-Math

  A series of math-specific large language models of our Qwen2 series.

  Language:Python59457

• facebookresearch/Evariste

  HyperTree Proof Search for Neural Theorem Proving -- "La science est l'œuvre de l'esprit humain, qui est plutôt destiné à étudier qu'à connaître, à chercher qu'à trouver la vérité."

  Language:Python342

• MingchaoZhu/DeepLearning

  Python for《Deep Learning》，该书为《深度学习》(花书) 数学推导、原理剖析与源码级别代码实现

  Language:Python6.5k1.3k

• zhaoxlpku/SubgoalXL

  Language:Python182

• MARIO-Math-Reasoning/Super_MARIO

  Language:Python24816

• OFA-Sys/gsm8k-ScRel

  Codes and Data for Scaling Relationship on Learning Mathematical Reasoning with Large Language Models

  Language:Python21916

• deepseek-ai/DeepSeek-Prover-V1.5

  Language:Python22524

• facebookresearch/searchformer

  Official codebase for the paper "Beyond A* Better Planning with Transformers via Search Dynamics Bootstrapping".

  Language:Jupyter Notebook32116

• FVELER/FVELerExtraction

  The FVELer dataset and code for extracting it.

  Language:Python1

• rookie-joe/PDA

  Language:Python18

• ufmg-smite/lean-smt

  Tactics for discharging Lean goals into SMT solvers.

  Language:Lean10420

• leanprover-community/duper

  Language:Lean548

• HEPLean/HepLean

  A project to digitalise results from high energy physics into Lean.

  Language:Lean724

• allenai/open-instruct

  Language:Python1.3k172

• pytorch/torchtune

  PyTorch native finetuning library

  Language:Python4.3k432

• kim-em/lean-training-data

  Language:Lean3611

• InternLM/InternLM-Math

  State-of-the-art bilingual open-sourced Math reasoning LLMs.

  Language:Python43726

• mortarsanjaya/IMOSLLean4

  Formalization of IMO shortlist problems in Lean 4

  Language:Lean132

• loganrjmurphy/LeanEuclid

  LeanEuclid is a benchmark for autoformalization in the domain of Euclidean geometry, targeting the proof assistant Lean.

  Language:Lean765

• cavalierlulu/rag_survey

  11911

• jinpz/refactor

  The official code release for REFACTOR: Learning to Extract Theorems from Proofs

  Language:Objective-C++51

• wiio12/POETRY

  Code for the paper: Proving Theorems Recursively

  11

• zhaoyu-li/DL4TP

  [COLM 2024] A Survey on Deep Learning for Theorem Proving

  1328

• hiyouga/LLaMA-Factory

  Unified Efficient Fine-Tuning of 100+ LLMs (ACL 2024)

  Language:Python34.4k4.2k

• filipmaric/IMO

  Formalization of IMO solutions in Isabelle/HOL

  Language:Isabelle8