The term "proof assistant" is usually used to describe a computer software that assists humans with developing formal proofs. A formal proof is a finite sequence of declarative sentences which are either:

• an axiom,
• an assumption,
• a sentence that follows from one or more of the previous sentences;

and the sequence of sentences must end with no more assumptions remaining.

This formal structure makes it easier for computers to parse and verify the proofs. An example of an alternative to a formal proof would be a natural language deduction.

The term "proof assistant" is usually used to describe a computer software that assists humans with developing formal proofs. A formal proof is a finite sequence of declarative sentences which are either:

• an axiom,
• an assumption,
• a sentence that follows from one or more of the previous sentences;

and the sequence of sentences must end with no more assumptions remaining.

This formal structure makes it easier for computers to parse and verify the proofs. An example of an alternative to a formal proof would be a natural language deduction.

This Stack Exchange site has some good resources to learn more about the basics of proof assistants:

• What's the "Hello, World!" for proof assistants?
• What are some examples of proof assistants doing something useful?
• What was the 1st Proof Assistant?