Is there any formal proof library or package? I am looking for a library or a package (in Python, C/C++ or whatever mainstream language) that allow to do some formal logic, such as carrying out proof verification, applying rules etc.
In an ideal world and in Python, something like this:
from logic import ZOL, FOL, HOL, Peano, ZFC, Z2 ...
ZOL.apply("Modus ponens", "(P -> Q)∧P")

Would return "Q"
print ZFC.axioms, ZFC.rules

Would print ZFC axioms and rules
Z2.check(someProof)

Would check the validity of some second order arithmetic proof etc.
So far I've only found whole framework with IDEs and lots of features such as Isabelle or COQ which are proof assistants. I have never found a single library or package, and have no idea how to easily expose the internal machinery of Isabelle to achieve such a result.
EDIT:
Maybe my question can simmply be restated as "Is there a way to use Isabelle or Coq or whatever as a library ?".
There are so many half dead projects. Or very living ones with fancy UI but no way to easily carry out the simple steps I described, in a world of github and open research this is hard to understand.
 A: Yes. Indeed, many theorem provers are implemented this way. In fact, Isabelle is implemented this way, or rather, Isabelle is essentially a variant of ML in which multiple other logical systems are implemented this way. Welder is a relatively recently created example using Scala as the host language.
The key idea here is an LCF-style theorem prover. Any programming language that can enforce abstraction (in the sense of abstract data types) can be used to make such a theorem prover. It's not even that hard to do. (For large scale work in practice, providing access to decision procedures and/or building a decent tactic library as well as a good amount of performance tuning is important.)
The idea is simple. You make an abstract data type Theorem. The only operations you define on type Theorem correspond to truth-preserving rules or axioms. You fail the operation (e.g. by throwing an exception or returning an error value) if it is a misapplication of a rule.
For example, here is a simple example for classical propositional logic in the language Haskell using the Hilbert-style axiomatization described on Wikipedia:
module PL(Formula(..), Theorem, k, s, contra, modusPonens, asFormula) where

data Formula
  = Var String
  | Not Formula
  | Formula :-> Formula
  deriving (Eq)

instance Show Formula where
    showsPrec _ (Var s) = (s++)
    showsPrec _ (Not f) = ('~':) . shows f
    showsPrec _ (p :-> q) = showParen True (shows p . (" -> "++) . shows q)

newtype Theorem = T { asFormula :: Formula }
    deriving (Eq)

instance Show Theorem where showsPrec n (T f) = showsPrec n f

k :: Formula -> Formula -> Theorem
k p q = T (p :-> (q :-> p))

s :: Formula -> Formula -> Formula -> Theorem
s p q r = T ((p :-> (q :-> r)) :-> ((p :-> q) :-> (p :-> r)))

contra :: Formula -> Formula -> Theorem
contra p q = T ((Not q :-> Not p) :-> (p :-> q))

modusPonens :: Theorem -> Theorem -> Maybe Theorem
modusPonens (T p) (T (p' :-> q)) | p == p' = Just (T q)
modusPonens     _              _           = Nothing

i :: Formula -> Maybe Theorem -- P -> P
i p = modusPonens (k p (p :-> p)) (s p (p :-> p) p) >>= modusPonens (k p p)

Since the Theorem data constructor, T, is not exported. The only way for consumers of this module to create a value of type Theorem is to use s, k, contra, or modusPonens. As long as I didn't make a mistake implementing those (and you can see it is a straightforward translation of the axioms and rules), then any value of type Theorem corresponds to a theorem of classical propositional logic. i is an example witnessing the statement from the Wikipedia page that the axiom they call "P1" is redundant. To check it, you would load this file into GHCi and type, say, i (Var "P"), and verify that it outputs Just (P -> P). Since Haskell has a REPL (GHCi), the result of this is an interactive theorem prover with a powerful tactic language (namely Haskell itself). You could do a similar thing in Python, say, though you would need to add run-time checks to verify that e.g. modusPonens's arguments were actually of type Theorem, and you'd have to assume the user does no reflection shenanigans or otherwise violates the abstraction boundary.
To handle more complicated logics or different presentations of this logic, you can just implement the rules directly as manipulations on syntax as I've done here. Or you can use literally whatever representation and algorithm you want as long as it preserves theoremhood. In practice, you'd likely want a notion of "conditional theoremhood", i.e. entailment, rather than unconditional theoremhood. It would be a minor change to extend the above code to do that.
