Formally-Verified-MultiObjective-Optimisation (It is still ongoing in a separate (closed-source) repo) Attempt to formalise this nice paper in semiring setting https://web.math.pmf.unizg.hr/glasnik/forthcoming/pGM6287.pdf