File size: 1,343 Bytes
4a274b5 3fb5bf5 |
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 |
---
license: mit
tags:
- formal-verification
- coq
- threshold-logic
- neuromorphic
---
# tiny-NOT-prover
Formally verified NOT gate. Single threshold neuron computing negation with 100% accuracy.
## Architecture
| Component | Value |
|-----------|-------|
| Inputs | 1 |
| Outputs | 1 |
| Neurons | 1 |
| Parameters | 2 |
| Weights | [-1] |
| Bias | 0 |
| Activation | Heaviside step |
## Key Properties
- 100% accuracy (2/2 inputs correct)
- Coq-proven correctness
- Single threshold neuron
- Integer weights
- Involutive: NOT(NOT(x)) = x
## Usage
```python
import torch
from safetensors.torch import load_file
weights = load_file('not.safetensors')
def not_gate(x):
# Heaviside: weighted_sum + bias >= 0
return int((x * weights['weight'] + weights['bias']) >= 0)
# Test
print(not_gate(0)) # 1
print(not_gate(1)) # 0
```
## Verification
**Coq Theorem**:
```coq
Theorem not_correct : forall x, not_circuit x = negb x.
```
Proven axiom-free. Full proof: [coq-circuits/Boolean/NOT.v](https://github.com/CharlesCNorton/coq-circuits)
## Citation
```bibtex
@software{tiny_not_prover_2025,
title={tiny-NOT-prover: Formally Verified NOT Gate},
author={Norton, Charles},
url={https://huggingface.co/phanerozoic/tiny-NOT-prover},
year={2025}
}
```
|