---
title: "jrh13/hol-light: papers citing this GitHub repository"
description: "8 papers in the tracked journals link to the GitHub repository jrh13/hol-light in their Crossref records, the first in 2016; most of them (1) in 2025."
url: https://scholar4ai.com/code/github-jrh13-hol-light
markdown_url: https://scholar4ai.com/code/github-jrh13-hol-light.md
license: CC BY-NC 4.0 (https://creativecommons.org/licenses/by-nc/4.0/)
share_text: "8 papers in the tracked journals link to the GitHub repository jrh13/hol-light in their Crossref records, the first in 2016; most of them (1) in 2025. (as of 2026-11-03)"
data_url: https://scholar4ai.com/data/rankings.json
updated: 2026-11-03T14:43:26+09:00
window: 2026-10-05 to 2026-11-03
source: OpenAlex (CC0)
---

# jrh13/hol-light: papers linking to it

Research papers in the 480 tracked journals that link to jrh13/hol-light (https://github.com/jrh13/hol-light), read from their Crossref records: by year, category and journal, the family tree of papers building on one another, and the linked repositories derived from it or that it derives from.

- GitHub
- 563 stars
- 100 forks
- OCaml
- created 2015
- https://github.com/jrh13/hol-light

All repositories: https://scholar4ai.com/code.md

## Key findings

- 8 papers in the tracked journals link to the GitHub repository jrh13/hol-light in their Crossref records, the first in 2016; most of them (1) in 2025.
- By category: AI (8); the journals with the most are Journal of Automated Reasoning (8).

## By year

*Papers linking to jrh13/hol-light by publication year*

| Year | Papers |
|---|---:|
| 2016 | 1 |
| 2017 | 1 |
| 2018 | 1 |
| 2020 | 1 |
| 2021 | 1 |
| 2023 | 1 |
| 2024 | 1 |
| 2025 | 1 |

## Journals

*Journals whose papers link to jrh13/hol-light most*

| Journal | Papers |
|---|---:|
| [Journal of Automated Reasoning](https://scholar4ai.com/journals/journal-of-automated-reasoning.md) | 8 |

## Papers

*Papers linking to jrh13/hol-light, most cited first*

| Published | Title | Journal | Authors | Citations | Link |
|---|---|---|---|---:|---|
| 2016-10-04 | [Fermat, Euler, Wilson - Three Case Studies in Number Theory](https://doi.org/10.1007/s10817-016-9387-z) | [Journal of Automated Reasoning](https://scholar4ai.com/journals/journal-of-automated-reasoning.md) | Christoph Walther, Nathan Wasser | 4 | cites it |
| 2018-12-04 | [Formalization of Geometric Algebra in HOL Light](https://doi.org/10.1007/s10817-018-9498-9) | [Journal of Automated Reasoning](https://scholar4ai.com/journals/journal-of-automated-reasoning.md) | Liming Li, Zhiping Shi, Yong Guan et al. | 3 | cites it |
| 2020-03-06 | [Formalization of Euler–Lagrange Equation Set Based on Variational Calculus in HOL Light](https://doi.org/10.1007/s10817-020-09549-w) | [Journal of Automated Reasoning](https://scholar4ai.com/journals/journal-of-automated-reasoning.md) | Yong Guan, Jingzhi Zhang, Guohui Wang et al. | 3 | cites it |
| 2025-02-18 | [Fast, Verified Computation for HOL ITPs](https://doi.org/10.1007/s10817-025-09719-8) | [Journal of Automated Reasoning](https://scholar4ai.com/journals/journal-of-automated-reasoning.md) | Oskar Abrahamsson, Magnus O. Myreen, Michael Norrish et al. | 3 | cites it |
| 2023-08-29 | [Mechanising Gödel–Löb Provability Logic in HOL Light](https://doi.org/10.1007/s10817-023-09677-z) | [Journal of Automated Reasoning](https://scholar4ai.com/journals/journal-of-automated-reasoning.md) | Marco Maggesi, Cosimo Perini Brogi | 2 | cites it |
| 2017-12-20 | [Distant Decimals of $$\\pi $$ π : Formal Proofs of Some Algorithms Computing Them and Guarantees of Exact Computation](https://doi.org/10.1007/s10817-017-9444-2) | [Journal of Automated Reasoning](https://scholar4ai.com/journals/journal-of-automated-reasoning.md) | Yves Bertot, Laurence Rideau, Laurent Théry | 1 | cites it |
| 2021-08-28 | [Distilling the Requirements of Gödel’s Incompleteness Theorems with a Proof Assistant](https://doi.org/10.1007/s10817-021-09599-8) | [Journal of Automated Reasoning](https://scholar4ai.com/journals/journal-of-automated-reasoning.md) | Andrei Popescu, Dmitriy Traytel | 1 | cites it |
| 2024-10-21 | [Windmills of the Minds: A Hopping Algorithm for Fermat’s Two Squares Theorem](https://doi.org/10.1007/s10817-024-09708-3) | [Journal of Automated Reasoning](https://scholar4ai.com/journals/journal-of-automated-reasoning.md) | Hing-Lun Chan | 0 | cites it |

## How this is measured

Links are read from each paper's Crossref record as its publisher deposited it: the URLs and repository DOIs in its reference list (the software and data it cites) and its supplementary links (“is-supplemented-by”: its own code or data). A paper that gives its code only in the text, a footnote or a data availability statement is not counted, and some publishers deposit reference lists without their URLs, so every count here is a lower bound. Repository details come from the GitHub REST API (stars, forks, and the repository a fork was made from), the Hugging Face Hub API (likes, downloads, and the base model a model was derived from) and DataCite (Zenodo and other data DOIs, and the GitHub release a Zenodo record archives), read again every month.

## Cite this page

Scholar4AI. (2026). jrh13/hol-light: papers linking to it. Journal and Conference Research Rankings. Retrieved November 3, 2026, from https://scholar4ai.com/code/github-jrh13-hol-light

```bibtex
@misc{scholar4ai-code-github-jrh13-hol-light,
  author = {{Scholar4AI}},
  title = {jrh13/hol-light: papers linking to it},
  year = {2026},
  howpublished = {\url{https://scholar4ai.com/code/github-jrh13-hol-light}},
  urldate = {2026-11-03},
  note = {Journal and Conference Research Rankings; data from OpenAlex (CC0); licensed CC BY-NC 4.0}
}
```

License: CC BY-NC 4.0 (https://creativecommons.org/licenses/by-nc/4.0/).