Lanyon AI may interest people here. Their approach uses an LLM to propose a formal specification in a domain-specific language, then generates code and proofs together through symbolic methods.
Their research notes include PDE solvers and benchmarks.
Has anyone explored this approach, or how it could fit with Julia/SciML workflows?
I know they’re working on a DSL for LLMs that would allow them to do verifiable scientific research, in particular physics in the same way Lean allows this for pure math. So I was wondering if Julia community could learn something from this.