연구진이 형식 수학과 비형식 수학을 연결하는 통합 의존성 그래프인 TheoremGraph를 발표했어요. arXiv 논문에서 1830만 개의 후보 의존성을 추출하고, Lean 프로젝트에서 388,105개의 선언 노드와 1130만 개의 유형 에지를 생성했어요. 자연어 슬로건을 공유된 의미 공간에 임베딩하여 논문과 형식/비형식 수학 간의 관련 진술을 연결하고, LLM 평가 결과 4만7952개의 매칭이 확인됐어요.