ProofPartner/CITATION.cff at master · crqu/ProofPartner · GitHub

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
cff-version: 1.2.0
message: "If you use ProofPartner in your research, please cite it as below."
title: "ProofPartner: An Agentic Mathematical Research Partner"
type: software
version: 0.1.0
date-released: "2026-07-09"
license: MIT
url: "https://github.com/crqu/ProofPartner"
repository-code: "https://github.com/crqu/ProofPartner"
keywords:
  - formal mathematics
  - theorem proving
  - Lean 4
  - conjecture generation
  - automated formalization
  - agentic AI
authors:
  - family-names: Qu
    given-names: Chengrui
    email: qcrpku@gmail.com
references:
  - type: article
    title: "Beyond the Library: An Agentic Framework for Autoformalizing Research Mathematics"
    authors:
      - family-names: Soltani Moakhar
        given-names: Arshia
      - family-names: Gholami
        given-names: Iman
      - family-names: Springer
        given-names: Max
      - family-names: JafariRaviz
        given-names: Mahdi
      - family-names: Hajiaghayi
        given-names: MohammadTaghi
    year: 2026
    url: "https://arxiv.org/abs/2606.31134"
    notes: "ProofPartner's proof pipeline incorporates the type-first formalization and auxiliary lemma validation techniques from this work."
  - type: article
    title: "LeanDojo: Theorem Proving with Retrieval-Augmented Language Models"
    authors:
      - family-names: Yang
        given-names: Kaiyu
      - family-names: Swope
        given-names: Aidan
      - family-names: Gu
        given-names: Alex
      - family-names: Chalamala
        given-names: Rahul
      - family-names: Song
        given-names: Peiyang
      - family-names: Yu
        given-names: Shixing
      - family-names: Godil
        given-names: Saad
      - family-names: Prenger
        given-names: Ryan
      - family-names: Anandkumar
        given-names: Anima
    year: 2023
    collection-title: "Advances in Neural Information Processing Systems (NeurIPS)"
  - type: dataset
    title: "miniF2F: A Cross-System Benchmark for Formal Olympiad-Level Mathematics"
    authors:
      - family-names: Zheng
        given-names: Kunhao
      - family-names: Han
        given-names: Jesse Michael
      - family-names: Polu
        given-names: Stanislas
    year: 2022