sci-mathematics

4ti2 1.6.10 ::gentoo 1 overlay Software package for algebraic, geometric and combinatorial problems
ExportSageNB 3.4 3 mo 1 overlay This is a tool to convert SageNB notebooks to other formats.
Oid 4.0-r1 1 overlay An interactive, extensible software system for experimenting with matroids
abc 0_p20230313 ::gentoo 1 overlay System for sequential logic synthesis and formal verification
acl2 8.6 ::gentoo 1 overlay Industrial strength theorem prover, logic and programming language
agda 2.8.0 6 mo 1 overlay A dependently typed functional programming language and proof assistant
agda-stdlib 2.8.0.2.3 6 mo 1 overlay Agda standard library
alectryon 2.0.0 ::gentoo 1 overlay Toolkit for literate programming in Coq/Rocq
alt-ergo 2.4.3-r3 ::gentoo 1 overlay Automatic theorem prover
arb 2.23.0 ::gentoo 1 overlay C library for arbitrary-precision interval arithmetic
atelier-b 24.04.2 50 d 1 overlay IDE for formal modelling and verification with the B method
b2program 0.1.0_p20260512 49 d 1 overlay Code generator from B to Java, C++, Python, Rust, and TypeScript
bertini 1.6 ::gentoo 1 overlay Software for Numerical Algebraic Geometry
btor2tools 1.0.0_pre20220518-r1 ::gentoo 1 overlay Generic parser and tools for the BTOR2 format
cadabra 2.5.14_p1-r1 ::gentoo 1 overlay Field-theory motivated approach to computer algebra
cadical 3.0.0 ::gentoo 1 overlay Simplified Satisfiability Solver
cado-nfs 2.3.0 2 mo 1 overlay Number Field Sieve (NFS) implementation for factoring integers
calc 2.17.0.0 36 d ::gentoo 2 overlays Arbitrary precision C-like arithmetic system
cgal 6.1 4 mo ::gentoo 2 overlays C++ library for geometric algorithms and data structures
cipi 1.0-r1 1 overlay Computing information projections iteratively
clipper2 1.5.4 ::gentoo 1 overlay Polygon Clipping and Offsetting
cliquer 1.23 ::gentoo 1 overlay C routines for finding cliques in an arbitrary weighted graph
coq 9.2.0 ::gentoo 1 overlay Coq/Rocq is a proof assistant written in O'Caml
coq-mathcomp 1.19.0-r1 ::gentoo 1 overlay Mathematical Components for the Coq proof assistant
coq-serapi 0.20.0 ::gentoo 1 overlay Serialization library and protocol for interaction with the Coq proof assistant
coq-stdlib 9.1.0 ::gentoo 1 overlay Stdlib for the Coq/Rocq Prover, used to be part of Coq
cryptominisat 5.11.21-r3 ::gentoo 1 overlay Advanced SAT solver with C++ and command-line interfaces
cu2 20060223 6 mo 1 overlay An non-optimal 2x2x2 rubik's cube solver
cubex 20060128 6 mo 1 overlay An non-optimal 3x3x3 rubik's cube solver
cubicle 1.2.0-r2 ::gentoo 1 overlay Model checker for verifying properties of array-based systems
cudd 3.0.0-r2 7 mo ::gentoo 2 overlays Colorado University binary Decision Diagram library
cvc4 1.8-r7 ::gentoo 1 overlay Automatic theorem prover for satisfiability modulo theories (SMT) problems
database_cubic_hecke 2022.4.4-r1 3 mo 1 overlay data for the representations of the Cubic Hecke Algebra
database_knotinfo 2026.3.1 2 mo 1 overlay Content of the KnotInfo & LinkInfo databases as lists of dictionaries
dataplot 20131220 ::gentoo 1 overlay Program for scientific visualization and statistical analyis
dikcube 20070912-r1 6 mo 1 overlay Dik T. Winter's rubik's cube solver and related tools
dolfinx 0.11.0 44 d 1 overlay Next generation FEniCS problem solving environment
dsfmt 2.2.4 ::gentoo 1 overlay Double precision SIMD-oriented Fast Mersenne Twister library
dunshire 0.1.3-r3 ::gentoo 1 overlay Python library to solve linear games over symmetric cones
easycrypt 2026.06 ::gentoo 1 overlay Computer-Aided Cryptographic Proofs
eclib 20250627 ::gentoo 1 overlay Programs for elliptic curves defined over the rational numbers
ent 101202 ::gentoo 1 overlay Random number sequence test and entropy calculation
eprover 3.2.5 ::gentoo 1 overlay Automated theorem prover for full first-order logic with equality
euler 1.61.0-r1 ::gentoo 1 overlay Mathematical programming environment
evbt 1.5.0 50 d 1 overlay Event-B tool for code generation and documentation
eventb-animate 6.3 2 d 1 overlay Animate Event-B models with the ProB model checker
eventb-checker 1.13 2 d 1 overlay Standalone validator for Event-B models
eventb-to-txt 1.7 50 d 1 overlay Convert Rodin Event-B models to plain-text format
fann 2.2.0-r2 ::gentoo 1 overlay Fast Artificial Neural Network Library
flint 3.5.0 ::gentoo 1 overlay Fast Library for Number Theory
flocq 4.2.1 ::gentoo 1 overlay Formalization of floating-point arithmetic for the Coq proof assistant
form 5.0.0 ::gentoo 1 overlay Symbolic Manipulation System
frama-c 25.0-r2 1 overlay Framework for analysis of source codes written in C
frama-c-aorai 25.0 1 overlay Aorai (automaton annotations) plugin for frama-c
frama-c-callgraph 25.0 1 overlay Callgraph plugin for frama-c
frama-c-constant-folding 25.0 1 overlay Constant folding plugin for frama-c
frama-c-dive 25.0 1 overlay Dive plugin for frama-c
frama-c-e-acsl 25.0 1 overlay Runtime verification of ACSL (E-ACSL) plugin for frama-c
frama-c-eva 25.0 1 overlay Value analysis (EVA) plugin for frama-c
frama-c-from 25.0 1 overlay From analysis plugin for frama-c
frama-c-impact 25.0 1 overlay Impact plugin for frama-c
frama-c-inout 25.0 1 overlay In/out analysis plugin for frama-c
frama-c-instantiate 25.0 1 overlay Instantiate analysis plugin for frama-c
frama-c-loopanalysis 25.0 1 overlay Loop analysis plugin for frama-c
frama-c-metrics 25.0 1 overlay Metrics plugin for frama-c
frama-c-nonterm 25.0 1 overlay Nonterm plugin for frama-c
frama-c-obfuscator 25.0 1 overlay Obfuscator plugin for frama-c
frama-c-occurrence 25.0 1 overlay Occurrence analysis plugin for frama-c
frama-c-pdg 25.0 1 overlay Program dependence graph plugin for frama-c
frama-c-postdominators 25.0 1 overlay Postdominators plugin for frama-c
frama-c-printapi 25.0 1 overlay Plugin generating .mli interface files for plugin APIs for frama-c
frama-c-qed 25.0 1 overlay Qed plugin for frama-c
frama-c-reduc 25.0 1 overlay frama-c plugin to generate ACSL annotations from Eva information
frama-c-report 25.0 1 overlay Report plugin for frama-c
frama-c-rtegen 25.0 1 overlay Runtime error annotation (RTE) generation plugin for frama-c
frama-c-scope 25.0 1 overlay Scope plugin for frama-c
frama-c-security-slicing 25.0 1 overlay Security slicing plugin for frama-c
frama-c-server 25.0 1 overlay Server plugin for frama-c
frama-c-slicing 25.0 1 overlay Slicing plugin for frama-c
frama-c-sparecode 25.0 1 overlay Spare code plugin for frama-c
frama-c-studia 25.0 1 overlay Studia plugin for frama-c
frama-c-users 25.0 1 overlay Users plugin for frama-c
frama-c-variadic 25.0 1 overlay Variadic function transformation plugin for frama-c
freefem++ 4.10 1 overlay Solve PDEs using FEM on 2d and 3d domains
fricas 1.3.13 ::gentoo 1 overlay FriCAS is a fork of Axiom computer algebra system
frobby 0.9.0-r4 ::gentoo 1 overlay Software system and project for computations with monomial ideals
functions-matlab-colormaps 1.0_p20250328 ::gentoo 1 overlay Additional colormaps for octave by Ultralytics
gap 4.16.0 ::gentoo 1 overlay System for computational discrete algebra (core functionality)
gappa 1.4.2 ::gentoo 1 overlay Tool for verifying floating-point or fixed-point arithmetic
gappalib-coq 1.5.3 ::gentoo 1 overlay Allows the certificates Gappa generates to be imported by the Coq
genius 1.0.29 ::gentoo 1 overlay Genius Mathematics Tool and the GEL Language
geogebra-bin 6.0.804.0-r1 ::gentoo 1 overlay Mathematics software for geometry
geomview 1.9.5-r1 ::gentoo 1 overlay Interactive Geometry Viewer
gfan 0.8_beta1 ::gentoo 1 overlay Compute Groebner fans and tropical varieties
giac 1.9.0.995-r2 2 yr ::gentoo 2 overlays A free C++ Computer Algebra System library and its interfaces
gimps 30.19.20 ::gentoo 1 overlay The Great Internet Mersenne Prime Search
ginac 1.8.10 ::gentoo 1 overlay C++ library and tools for symbolic calculations
glpk 5.0-r4 ::gentoo 1 overlay GNU Linear Programming Kit
gmm 5.4.2 ::gentoo 1 overlay Generic C++ template library for sparse, dense and skyline matrices
gmp-ecm 7.0.6-r1 ::gentoo 1 overlay Elliptic Curve Method for Integer Factorization
gp2c 0.0.14 ::gentoo 1 overlay A GP to C translator
gretl 2021d ::gentoo 1 overlay Regression, econometrics and time-series library
gsl-shell 2.3.5 ::gentoo 1 overlay Lua interactive shell for sci-libs/gsl
highs 1.14.0-r3 ::gentoo 1 overlay Modern solver for linear, quadratic, and mixed-integer programs
hom4ps-bin 2 2 yr 1 overlay HOMotopy method for solving Polynomial Systems
jags 4.3.1-r1 ::gentoo 1 overlay Just Another Gibbs Sampler for Bayesian MCMC simulation
kind2 1.9.0 ::gentoo 1 overlay Multi-engine SMT-based automatic model checker
kissat 4.0.4 ::gentoo 1 overlay Keep-it-simple and clean bare metal SAT solver written in C
latte-int 1.7.6 24 mo 1 overlay latte-int(egrale) consists of tools for lattice point enumeration
lcalc 2.1.1 ::gentoo 1 overlay Command-line utility and library for L-function computations
lean 4.24.0 21 mo ::gentoo 2 overlays The Lean Theorem Prover
libpoly 0.1.11 ::gentoo 1 overlay C library for manipulating polynomials
libsfmt 1.3.0 1 overlay SIMD-oriented Fast Mersenne Twister
lie 2.2.2 24 mo 2 overlays A Computer algebra package for Lie group computations
lpsolve 5.5.2.14 ::gentoo 1 overlay Mixed Integer Linear Programming (MILP) solver
lrcalc 2.1 ::gentoo 1 overlay Littlewood-Richardson Calculator
ltl2ba 1.3 1 overlay Fast LTL to Buechi Automata Translation
ltsmin 3.0.2 8 d 1 overlay High-performance language-independent model checking tools
manifold 3.2.1 ::gentoo 1 overlay Geometry library for topological robustness
mathematica 14.3.0-r1 7 mo ::gentoo 4 overlays Wolfram Mathematica
mathmod 13.0-r1 ::gentoo 1 overlay Plot parametric and implicit surfaces
mathomatic 16.0.5-r1 ::gentoo 1 overlay Automatic algebraic manipulator
matroid-database 0.3-r1 3 mo 1 overlay Yoshitake Matsumoto, Database of Matroids
maxima 5.49.0 ::gentoo 1 overlay Free computer algebra environment based on Macsyma
mcube 20051209 6 mo 1 overlay An non-optimal 4x4x4 rubik's cube solver
metamath 0.198 ::gentoo 1 overlay Proof verifier based on a minimalistic formalism
metamath-databases 20220303 ::gentoo 1 overlay Sample databases for Metamath
minisat 2.2.1-r1 ::gentoo 1 overlay Small yet efficient SAT solver with reference paper
modular_resolution 1.1-r1 24 mo 1 overlay p_group_cohomology helper library
msieve 1.53-r3 ::gentoo 1 overlay A C library implementing a suite of algorithms to factor large integers
nauty 2.8.8-r1 ::gentoo 1 overlay Computing automorphism groups of graphs and digraphs
nestedsums 1.5.2-r1 ::gentoo 1 overlay A GiNaC-based library for symbolic expansion of certain transcendental functions
normaliz 3.11.0 ::gentoo 1 overlay Tool for computations in affine monoids and more
num-utils 0.5-r2 ::gentoo 1 overlay A set of programs for dealing with numbers from the command line
octave 11.1.0 2 yr ::gentoo 2 overlays High-level interactive language for numerical computations
octave-epstk 2.4 ::gentoo 1 overlay Graphical output functions for Matlab and Octave
octave-jsonlab 2.9.8 24 mo 1 overlay JSONLab: compact, portable, robust JSON/binary-JSON encoder/decoder for MATLAB/Octave
octave-meta 20221117-r1 13 mo 1 overlay Merge this to pull in all octave forge packages
opensmt 2.9.2 ::gentoo 1 overlay Compact and open-source SMT-solver written in C++
optimal 20040603-r1 6 mo 1 overlay An optimal rubik's cube solver using God's Algorithm
otter 3.3-r4 ::gentoo 1 overlay An Automated Deduction System
palp 2.21 ::gentoo 1 overlay A Package for Analyzing Lattice Polytopes (PALP)
pari 2.17.2 ::gentoo 1 overlay Computer-aided number theory C library and tools
pari-data 20191216 ::gentoo 1 overlay Additional dataset packages for PARI
petsc 3.25.1 ::gentoo 1 overlay Portable, Extensible Toolkit for Scientific Computation
picosat 965 ::gentoo 1 overlay SAT solver with proof and core support
planarity 5.0.0.0-r2 ::gentoo 1 overlay The edge addition planarity suite of graph algorithms
plfit 1.0.1 ::gentoo 1 overlay Fit power-law distributions to empirical data
polymake 4.15 ::gentoo 1 overlay Tool for polyhedral geometry and combinatorics
primecount 8.0 ::gentoo 1 overlay Highly optimized CLI and library to count primes
primesieve 12.3 ::gentoo 1 overlay CLI and library for quickly generating prime numbers
prng 3.0.2-r4 ::gentoo 1 overlay Pseudo-Random Number Generator library
prob-bin 1.15.1-r1 8 d 1 overlay Animator, constraint solver and model checker for B, Event-B, CSP, TLA+, Z
prob2-ui 1.3.1-r1 8 d 1 overlay JavaFX-based animator and model checker built on ProB
prover9 2009.11a-r2 ::gentoo 1 overlay Automated theorem prover for first-order and equational logic
proverif 2.05 ::gentoo 1 overlay Cryptographic protocol verifier in the formal model
psmt2-frontend 0.4.0 ::gentoo 1 overlay Library to parse and type-check an extension of the SMT-LIB 2 standard
pspp 2.0.1-r1 ::gentoo 1 overlay Program for statistical analysis of sampled data
pulp 3.1.1 1 overlay Create MPS/LP files, call solvers, and present results
pyromaths 21.8.2-r1 1 overlay Create maths exercises in LaTeX and PDF format
reduce 20240812 38 d 1 overlay A general-purpose computer algebra system
rink 0.9.0-r1 1 overlay Unit conversion tool, similar to frink
ripser 1.1 1 overlay efficient computation of Vietoris-Rips persistence barcodes
rkward 0.8.3 ::gentoo 2 overlays IDE for the R-project
rngstreams 1.0.1 2 yr ::gentoo 2 overlays Multiple independent streams of pseudo-random numbers
rodin 3.10.0 26 d 1 overlay IDE for formal modelling and verification with Event-B
rodin-headless 4.0 33 d 1 overlay Headless toolchain to build, model-check, and prove Rodin Event-B models
rossi 0.1.7 26 h 1 overlay Rust toolchain for Event-B: parser, static checker, CLI, and language server
rstudio-desktop-bin 2026.07.0_p139 9 d 2 overlays RStudio IDE for R (open-source desktop edition, prebuilt)
rw 0.9 ::gentoo 1 overlay Compute rank-width decompositions of graphs
sage-data-combinatorial_designs 20140630 6 mo 1 overlay Data for Combinatorial Designs
sage-data-elliptic_curves 0.8.1 3 mo 1 overlay Sage's elliptic curves databases
sage-data-graphs 20210214 6 mo 1 overlay Sage's graph database
sage-data-polytopes_db 20170220 6 mo 1 overlay Sage's polytopes database
sage-flatsurf 0.8.0 6 mo 1 overlay package for working with flat surfaces in SageMath.
sagemath 10.9-r1 10 d 1 overlay Math software for abstract and numerical computations
sagemath-doc 10.9 2 mo 1 overlay Build the sage documentation
sagemath-giac 0.1.4 3 mo 1 overlay Support using Giac in sagemath
scilab-bin 2023.1.0 1 overlay Scientific software package for numerical computations
sha1-polyml 5.9 ::gentoo 1 overlay implementation of SHA1 is taken from the GNU coreutils package
shared_meataxe 1.0.1-r1 2 yr 1 overlay A library and set of programs for working with matrices over finite fields
singular 4.4.1-r1 ::gentoo 1 overlay Computer algebra system for polynomial computations
slepc 3.25.1 ::gentoo 1 overlay Scalable Library for Eigenvalue Problem Computations
smtinterpol 2.5_p20211018-r1 ::gentoo 1 overlay Interpolating SMT-solver computing Craig interpolants for various theories
sofastatistics 1.5.7 2 mo 1 overlay SOFA is a statistics, analysis, and reporting program
spin 6.5.2-r1 ::gentoo 1 overlay An efficient logic-model checker for the verification of multi-threaded code
spline3 1.0.2 6 mo 1 overlay parallel implementation of the Sorokina/Zeilfelder spline scheme
stp 2.3.4-r1 ::gentoo 1 overlay Simple Theorem Prover, an efficient SMT solver for bitvectors
surface-dynamics 0.7.0 7 mo 1 overlay This sagemath package adds various functionality
sylvan 1.1.1 8 d 1 overlay Parallel decision diagram library
symbolica 0.16.0 16 mo 1 overlay A blazing fast computer algebra system.
symbolica-community 0.1.0 16 mo 1 overlay A blazing fast computer algebra system with community enhancements
sympow 2.023.7 ::gentoo 1 overlay Symmetric power elliptic curve L-functions
tlc4b 1.2.3 50 d 1 overlay Model-check classical B specifications by translating them to TLA+
topcom 1.1.2 ::gentoo 1 overlay Computing Triangulations Of Point Configurations and Oriented Matroids
twelf 1.7.1-r2 ::gentoo 1 overlay Implementation of the logical framework LF
unuran 1.11.0 2 yr ::gentoo 2 overlays Universal Non-Uniform Random number generator
vampire 5.0.1 ::gentoo 1 overlay The Vampire Prover, theorem prover for first-order logic
verifpal 0.27.0 ::gentoo 1 overlay Cryptographic protocol analysis for real-world protocols
verit 2021.06.2 ::gentoo 1 overlay An open, trustable and efficient SMT-prover
why3 1.8.2 ::gentoo 1 overlay Platform for deductive program verification
why3-for-spark 2023.12.13-r2 ::gentoo 1 overlay SPARK 2014 repository for the Why3 verification platform
wxmaxima 26.06.2 ::gentoo 1 overlay Graphical frontend to Maxima, using the wxWidgets toolkit
yacas 1.9.1-r3 ::gentoo 1 overlay General purpose computer algebra system
yafu 1.34.3-r2 ::gentoo 1 overlay Yet another factoring utility
yices2 2.7.0 ::gentoo 1 overlay SMT Solver supporting SMT-LIB and Yices specification language
z3 5.0.0 ::gentoo 1 overlay An efficient theorem prover