AI Rust Implementations

[phaynes]

Hi,

I have been developing experimental teaching programs aimed at helping students use AI systems to undertake advanced mathematics, science and engineering work.

As part of this, I have developed a verification-oriented AI software factory in Rust. I have also used it to build a Rust-based reimplementation of PicoGK-style functionality, since the verification system uses Rust and Lean as core technologies.

I do not want to disrupt the excellent work already happening here, but I wanted to ask whether contributions in this direction would be of interest.

Kind regards,
Philip

Rocket Project

[coolbluewater]

Hi - the Rust reimplementation sounds very interesting. Does it re-implement the C++ library as well as the C# functionality?

[phaynes]

I just did the easiest thing and re-wrote the C# as a PoC. Were the C++ source available, then that would be easy.

I also started porting different libraries such as NASA's CEA thermodynamics library and planned out a process to complete a full physical simulation environment.
Currently, I am starting to build out lean proofs of the underlying physics so the larger goal has a solid mathematical foundation.

[coolbluewater]

Were the C++ source available, then that would be easy.

Hmm, the C++ runtime is at https://github.com/leap71/PicoGKRuntime.

I also started porting different libraries such as NASA's CEA thermodynamics library and planned out a process to complete a full physical simulation environment.
Currently, I am starting to build out lean proofs of the underlying physics so the larger goal has a solid mathematical foundation.

Awesome. Sounds like you're already thinking quite far ahead.

[phaynes]

mmm - missed that - thanks!

Having worked through the problem space - all I see an enormously fun, and ridiculously large opportunity.

I will pop up a git repo over the next couple of days, and example physics proofs and my thoughts on where this goes.

[coolbluewater]

Curious about how the rust API turned out. Do you envision this to be a one-time port?
Also, what did you do for the viewer?
Maybe this discussion should continue in your repo once it's available.