Collaborative Theorem Proving with Large Language Models: Enhancing Formal Proofs with ProofRefiner

The paper is desk rejected for significant textual overlap with [1]. This decision was confirmed by multiple members of the program committee. Table 1 in both papers is identical. The related work sections also have significant overlap. The amount of textual overlap without proper attribution makes this a case of plagiarism.

[1] Towards Large Language Models as Copilots for Theorem Proving in Lean by Peiyang Song et al. https://arxiv.org/pdf/2404.12534