Automation for building lean skeletons

Stream: lean4

[Georgy C Luke]

What is the best approach to create a lean skeleton for proving theorems related to checking logical soundness of a particular context based on some text? Is using an LLM the best approach know so far or are there any tools? I guess Aristotle by Harmonic is a good such tool.