Suggestions for a tool to aid formalization

Stream: new members

[Chintan Bhat]

Hello everyone!
I'm currently working on a tool that takes in the DOI of a mathematics paper, and tries to identify the citation intention (dependent/non-dependent citation) for each citation. Then, it creates a Directed Acyclic Graph of the true dependencies of a paper.
Since LLMs are not great at understanding the intention of the citation, I will add a "Justification" feature, in which the user can click on an edge in the graph to find the LLM's justification why it classified a citation intent as dependent (result).
I have 2 questions for the community:
1) Would such a tool be useful?
2) What features would make it more useful for formalization? (It's okay if you give a suggestion that would be useful but much different from the tool I'm currently working on)

Thanks in advance!

[Kenny Lau]

Chintan Bhat said:

LLMs are not great at understanding the intention of the citation

Why wouldn't they be?

[Chintan Bhat]

I tried some papers with Gemini 2.5 Pro, and it seemed to look at only the surrounding text for indications that it is a dependent citation. But you're absolutely right - with better prompting and instructions, they can definitely do better.
I think Justification would be a useful feature nevertheless...

[Ruben Van de Velde]

I'm not really sure what this would be used for in the context of formalization

[Chintan Bhat]

It could be used as a quick tool to make a "first approximation" of a blueprint, to assess the feasibility of formalizing existing papers.
Again, the goal is to make a tool that is actually very useful for formalization, so feel free to suggest other approaches (or features) that you think will help the community more than my current approach.

[Ruben Van de Velde]

I wonder if doing this on a paper level rather than a theorem level won't be too much of an overapproximation

[Chintan Bhat]

Ruben Van de Velde said:

I wonder if doing this on a paper level rather than a theorem level won't be too much of an overapproximation

Thank you for the insight! I understand a theorem-level approximation would be significantly more useful. But if there were a theorem-level approximation, how useful do you think it would be? As in, how much time could it approximately save?