@misc{hardlab_beyond_correctness,
  title = {{Beyond Correctness: Toward Automated Novelty Verification with Lean 4}},
  author = {Ayrton Porto},
  year = {2026},
  eprint = {2608.14669},
  archivePrefix = {arXiv},
  doi = {10.48550/arXiv.2608.14669},
  url = {https://arxiv.org/abs/2608.14669},
  note = {External related work; metadata checked 2026-09-10}
}

@misc{hardlab_pythagoras,
  title = {{Pythagoras-Prover: Advancing Efficient Formal Proving via Augmented Lean Formalisation}},
  author = {Joshua Ong Jun Leang and Zheng Zhao and Mihaela Cătălina Stoian and Qiyuan Xu and Haonan Li and Wenda Li and Shay B. Cohen and Eleonora Giunchiglia},
  year = {2026},
  eprint = {2606.12594},
  archivePrefix = {arXiv},
  doi = {10.48550/arXiv.2606.12594},
  url = {https://arxiv.org/abs/2606.12594},
  note = {External related work; metadata checked 2026-09-10}
}

@misc{hardlab_leap,
  title = {{LEAP: Supercharging LLMs for Formal Mathematics with Agentic Frameworks}},
  author = {Po-Nien Kung and Linfeng Song and Dawsen Hwang and Jinsung Yoon and Chun-Liang Li and Simone Severini and Mirek Olšák and Edward Lockhart and Quoc V Le and Burak Gokturk and Thang Luong and Tomas Pfister and Nanyun Peng},
  year = {2026},
  eprint = {2606.03303},
  archivePrefix = {arXiv},
  doi = {10.48550/arXiv.2606.03303},
  url = {https://arxiv.org/abs/2606.03303},
  note = {External related work; metadata checked 2026-09-10}
}

@misc{hardlab_deepseek_prover,
  title = {{DeepSeek-Prover-V2: Advancing Formal Mathematical Reasoning via Reinforcement Learning for Subgoal Decomposition}},
  author = {Z.Z. Ren and Zhihong Shao and Junxiao Song and Huajian Xin and Haocheng Wang and Wanjia Zhao and Liyue Zhang and Zhe Fu and Qihao Zhu and Dejian Yang and Z.F. Wu and Zhibin Gou and Shirong Ma and Hongxuan Tang and Yuxuan Liu and Wenjun Gao and Daya Guo and Chong Ruan},
  year = {2025},
  eprint = {2504.21801},
  archivePrefix = {arXiv},
  doi = {10.48550/arXiv.2504.21801},
  url = {https://arxiv.org/abs/2504.21801},
  note = {External related work; metadata checked 2026-09-10}
}

@misc{hardlab_leandojo,
  title = {{LeanDojo: Theorem Proving with Retrieval-Augmented Language Models}},
  author = {Kaiyu Yang and Aidan M. Swope and Alex Gu and Rahul Chalamala and Peiyang Song and Shixing Yu and Saad Godil and Ryan Prenger and Anima Anandkumar},
  year = {2023},
  eprint = {2306.15626},
  archivePrefix = {arXiv},
  doi = {10.48550/arXiv.2306.15626},
  url = {https://arxiv.org/abs/2306.15626},
  note = {External related work; metadata checked 2026-09-10}
}