The sci-mathematics category contains mathematical software.

4ti2Software package for algebraic, geometric and combinatorial problems
abcSystem for sequential logic synthesis and formal verification
acl2Industrial strength theorem prover, logic and programming language
alectryonToolkit for literate programming in Coq
alt-ergoAutomatic theorem prover
arbC library for arbitrary-precision interval arithmetic
bertiniSoftware for Numerical Algebraic Geometry
boolectorFast SMT solver for bit-vectors, arrays and uninterpreted functions
btor2toolsGeneric parser and tools for the BTOR2 format
cadabraField-theory motivated approach to computer algebra
cadicalSimplified Satisfiability Solver
calcArbitrary precision C-like arithmetic system
cgalC++ library for geometric algorithms and data structures
cliquerC routines for finding cliques in an arbitrary weighted graph
coqProof assistant written in O'Caml
coq-mathcompMathematical Components for the Coq proof assistant
coq-serapiSerialization library and protocol for interaction with the Coq proof assistant
cryptominisatAdvanced SAT solver with C++ and command-line interfaces
cubicleModel checker for verifying properties of array-based systems
cuddColorado University binary Decision Diagram library
cvc4Automatic theorem prover for satisfiability modulo theories (SMT) problems
dataplotProgram for scientific visualization and statistical analyis
diagrtbCalculation of some eigenvectors of a large real, symmetrical, matrix
dsfmtDouble precision SIMD-oriented Fast Mersenne Twister library
dunshirePython library to solve linear games over symmetric cones
easycryptComputer-Aided Cryptographic Proofs
eclibPrograms for elliptic curves defined over the rational numbers
entRandom number sequence test and entropy calculation
eproverAutomated theorem prover for full first-order logic with equality
eulerMathematical programming environment
fannFast Artificial Neural Network Library
flintFast Library for Number Theory
flocqFormalization of floating-point arithmetic for the Coq proof assistant
formSymbolic Manipulation System
fricasFriCAS is a fork of Axiom computer algebra system
frobbySoftware system and project for computations with monomial ideals
gapSystem for computational discrete algebra. Core functionality.
gappaTool for verifying floating-point or fixed-point arithmetic
gappalib-coqAllows the certificates Gappa generates to be imported by the Coq
geniusGenius Mathematics Tool and the GEL Language
geogebra-binMathematics software for geometry
geomviewInteractive Geometry Viewer
gfanCompute Groebner fans and tropical varieties
giacA free C++ Computer Algebra System library and its interfaces
gimpsThe Great Internet Mersenne Prime Search
ginacC++ library and tools for symbolic calculations
glpkGNU Linear Programming Kit
gmmGeneric C++ template library for sparse, dense and skyline matrices
gmp-ecmElliptic Curve Method for Integer Factorization
gp2cA GP to C translator
gretlRegression, econometrics and time-series library
gsl-shellLua interactive shell for sci-libs/gsl
jagsJust Another Gibbs Sampler for Bayesian MCMC simulation
kind2Multi-engine SMT-based automatic model checker
kissatKeep-it-simple and clean bare metal SAT solver written in C
lcalcCommand-line utility and library for L-function computations
leanThe Lean Theorem Prover
libpolyC library for manipulating polynomials
lpsolveMixed Integer Linear Programming (MILP) solver
lrcalcLittlewood-Richardson Calculator
mathematicaWolfram Mathematica
mathlib-toolsDevelopment tools for Lean's mathlib
mathmodPlot parametric and implicit surfaces
mathomaticAutomatic algebraic manipulator
maximaFree computer algebra environment based on Macsyma
metamathProof verifier based on a minimalistic formalism
metamath-databasesSample databases for Metamath
minisatSmall yet efficient SAT solver with reference paper
msieveA C library implementing a suite of algorithms to factor large integers
nautyComputing automorphism groups of graphs and digraphs
nestedsumsA GiNaC-based library for symbolic expansion of certain transcendental functions
normalizTool for computations in affine monoids and more
num-utilsA set of programs for dealing with numbers from the command line
octaveHigh-level interactive language for numerical computations
octave-epstkGraphical output functions for Matlab and Octave
opensmtCompact and open-source SMT-solver written in C++
otterAn Automated Deduction System
palpA Package for Analyzing Lattice Polytopes (PALP)
pariComputer-aided number theory C library and tools
pari-dataAdditional dataset packages for PARI
petscPortable, Extensible Toolkit for Scientific Computation
picosatSAT solver with proof and core support
planarityThe edge addition planarity suite of graph algorithms
plfitFit power-law distributions to empirical data
polymakeTool for polyhedral geometry and combinatorics
primecountHighly optimized CLI and library to count primes
primesieveCLI and library for quickly generating prime numbers
prngPseudo-Random Number Generator library
prover9Automated theorem prover for first-order and equational logic
proverifCryptographic protocol verifier in the formal model
psmt2-frontendLibrary to parse and type-check an extension of the SMT-LIB 2 standard
psppProgram for statistical analysis of sampled data
rkwardIDE for the R-project
rngstreamsMultiple independent streams of pseudo-random numbers
rwCompute rank-width decompositions of graphs
sha1-polymlimplementation of SHA1 is taken from the GNU coreutils package
singularComputer algebra system for polynomial computations
slepcScalable Library for Eigenvalue Problem Computations
smtinterpolInterpolating SMT-solver computing Craig interpolants for various theories
spinAn efficient logic-model checker for the verification of multi-threaded code
stpSimple Theorem Prover, an efficient SMT solver for bitvectors
sympowSymmetric power elliptic curve L-functions
topcomComputing Triangulations Of Point Configurations and Oriented Matroids
twelfImplementation of the logical framework LF
unuranUniversal Non-Uniform Random number generator
vampireThe Vampire Prover, theorem prover for first-order logic
verifpalCryptographic protocol analysis for real-world protocols
veritAn open, trustable and efficient SMT-prover
why3Platform for deductive program verification
why3-for-sparkPlatform for deductive program verification
wxmaximaGraphical frontend to Maxima, using the wxWidgets toolkit
yacasGeneral purpose computer algebra system
yafuYet another factoring utility
yices2SMT Solver supporting SMT-LIB and Yices specification language
z3An efficient theorem prover


Packages: 115

Filter by Category