Open source · Lean 4 + Mathlib
lean-mechanics
Open-source Lean 4 library: tensors, kinematics, stress, constitutive laws, elastostatics, beams and plates, plus a formalised 2013 paper. No sorry, no axioms.
Papers · Open source
Research we publish in the open.
Our published papers, from reciprocal frames to tall buildings in the wind, and the theory behind structural design proved in the Lean theorem prover.
- lean-mechanics on GitHub github.com/raphos-com
- Research papers ResearchGate
Engineering software rests on theory that is usually trusted rather than checked: tensor identities, energy principles, closed-form solutions, homogenized stiffnesses. We formalise that theory in Lean 4 on top of Mathlib, so every statement is verified by a proof checker, down to the axioms.
The work is public on GitHub. It started from our own research on reciprocal frames, published at IASS 2013, and grew into a general library of continuum mechanics and structural theories.
Each of our papers has its own page below: structural homogenization, computational architecture, gridshell layout, machine learning for steel design, and full-scale wind monitoring of a London tower.
In this area
7 projects.
Open any project for the full write-up, capabilities and links.
Paper · IASS 2013, Wrocław
Elastic behaviour of reciprocal systems by homogenization
Greco, Lebée and Douthe (IASS 2013): the square nexorade homogenized as a plate, with closed-form stiffness and an optimal cell geometry. Every result is now a Lean theorem.
Poster · AAG 2014
A free-form roof for the Scuola Normale Superiore
Greco, Bevilacqua and Croce (AAG 2014): a funnel-shaped glass and steel roof for the Scuola Normale Superiore courtyard, from form finding to panel moulds and sized beams.
Paper · IASS 2018, MIT
Optimized quad gridshells from stress and curvature fields
Greco (IASS 2018): quad-only gridshells whose edges follow principal stresses and principal curvatures at once, built on CGAL and libigl in the Capybara plugin.
Paper · IASS 2018, MIT
Machine learning and optimization for steel connections
Greco (IASS 2018): machine-learning models trained on Eurocode 3 designs that predict steel end-plate connections, tested on a real London project.
Paper · UK Wind Engineering 2018
Wind-induced response of a slender tall building in London
Margnelli, Greco, Gkoktsi et al. (2018): nine months of full-scale monitoring on a slender 47-storey tower in London, with damping and response identified from the data.
Paper · 2019
Full-scale identification of aeroelastic effects on a tall building
Gonzalez-Fernandez, Macdonald, Titurus, Greco, Zanchetta et al. (2019): identifying aeroelastic effects on a tall building from full-scale data.
Want something like this for your team?
We build computational tools and software for hard engineering problems.