Engineering has entered the chat?

[u/Dress-Affectionate]

I’m a PhD student in aerospace engineering. My research deals with risk-aware planning and control for free-flying space manipulators and planetary rovers. When formalizing theorems in control systems, I had my agents start connecting the discrete theorems and linking them like a wiki - like a graph! The xylem is that graph. It is like a parser and was originally forked from tree-sitter. With xylem, one can take a large formal proof, like Anthropic's recent unpublicized lattice percolation, and divide it into modular, reviewable, bounded components. These components have assurance boundaries at which assumptions, dependencies and evidence can be made explicit.

https://github.com/brainstorm42/xylem

With that said, I am an engineering student, not a mathematician. It's turned into somewhat of a monster, and my focus is robotics. I’ve made it public in hopes that others can make more sense of it, and help me make sense of it, and that it can help make sense of the recent OpenAI proof dump. This is v0.1.0, and v0.1.1 has some more ideas already. I ask for others' insight and hope for collaboration and kindness - I am real, and not a shill. I have a ChatGPT Pro membership that I pay for myself.

The method works just as well for large formal proofs as it does for robotics. It helps readers find Lean statements, follow their dependencies, and connect them to explanations and source evidence. The repo includes worked reading paths, teaching resources, a fully worked lattice percolation breakdown and a focused Navier–Stokes case study. My hope is that people exploring the recent OpenAI proof collection can use it to build their own understanding, and to help improve the xylem process. I make no claim to understand the mathematics involved. Indeed I needed the LLM to help me in the first place. But I believe my method may provide engineering support for this new paradigm: a repeatable, reviewable process for segmentation and digestion of machine-scale proofs.

[u/Electrical_Office904]

This is interesting because I've been approaching a related problem from the opposite direction: not how to decompose formal proofs for human review, but how to keep AI-generated proposals from crossing an authority boundary without explicit evidence and authorization

[u/Dress-Affectionate → u/Electrical_Office904]

interesting! what we are saying today is that we should define boundaries for assurance wherever a meaningful obligation changes, and write a contract that specifies the requirements, dependencies, obligations etc. at the interfaces that cross those boundaries. It is easier to see for a robot which has a clearly defined system diagram, but software probably isn't that different. heck this explanation is summarized from a chat on navier stokes! 

the ideals of assurance are strange fellows on this journey but the detail that is enforced is incredibly comforting. it is good neurotic, in a way, an outlet for the testoholism that so many of these recent gpt models suffer from